Dedication: 题献

Preface: 前言

逻辑与计算之间最深刻的联系是一种双关。「命题即类型（Propositions as Types）」 的学说断言，形式化的结构可以按两种方式看待：可以看做逻辑中的命题， 也可以看做计算中的类型。此外，相关的结构可以看做命题的证明或者其相应类型的程序。 更进一步来说，证明的化简与程序的求值对应。

与此相应，本书的名字也有两种含义。它可以看做「编程语言的基础」，也可以看做 「编程的语言基础」。我们用 Agda 证明助理编写的规范（Specification） 同时描述了编程语言以及该语言编写的程序自身。

本书面向本科最后一年的学生、一年级的研究生或博士生。 本书以简单类型 λ-演算（Simply-Typed Lambda Calculus，简称 STLC）作为核心示例， 旨在教授编程语言的操作语义基础。全书以 Agda 文学脚本（Literal Script）的形式写成。 使用证明助理可以让开发过程变得更加具体而清晰易懂，还可以给予学生即时反馈， 帮助学生发现理解有误的地方并及时纠正。

【译注：文学编程（Literal Programming）用带有代码的自然语言文章来进行编程， 此概念由高德纳（Donald Knuth）提出，详情可参考维基百科。】

本书分为两册。第一分册为逻辑基础，发展了所需的形式化工具。第二分册为编程语言基础， 介绍了操作语义的基本方法。

个人评论

从 2013 年开始，我在爱丁堡大学为四年制本科生和研究生教授编程语言的类型和语义的课程。 该课程的早期版本基于 Benjamin Pierce 的著作 TAPL。我的版本则基于 Pierce 的后续教材《软件基础》（英文版 Software Foundations），此书为 Pierce 与他人合著，基于 Coq 编写。正如 Pierce 在 ICFP 的主题演讲 Lambda, The Ultimate TA 中所言，我也相信基于证明助理的课程会对学习有所帮助。

然而有了五年的教学经验后，我发现 Coq 并不是最好的授课载体。 对于学习编程语言理论基础而言，我们花费了太多课程去专门学习证明推导的策略（Tactic）。 每个概念都需要学习两遍：例如，在学过一遍积数据类型（Product Data Type）之后， 我们还要再学一遍与之对应的合取（Conjunction）的引入（Introduction）和消除（Elimination）策略。 Coq 用来生成归纳假设（Induction Hypothesis）的规则有时看起来很玄学。而 notation 构造则允许直观但灵活多变的语法，同一个概念总是有两个名字有时会令人迷惑， 例如，subst N x M 和 N [x := M]。策略的名字时短时长；标准库中的命名约定则非常不一致。 命题即类型作为证明的基础虽然存在，但却被雪藏了。

我发现自己热衷于用 Agda 重构此课程。在 Agda 中，我们不再需要学习策略了： 这里只有依值类型编程，简单纯粹。我们总是通过构造子来引入，通过模式匹配来消除。 归纳不再是谜之独立的概念，它与我们熟悉的递归概念直接对应。混缀语法十分灵活， 但每个概念只需要一个名字，例如代换就是 _[_:=_]。标准库虽不完美，但它的一致性却很合理。 命题即类型作为证明的基础则被骄傲地展示了出来。

不过，此前还没有用 Agda 语言描述的编程语言理论教材。虽然 Stump 的 Verified Functional Programming in Agda 涵盖了相关的范围， 但比起编程语言理论，却更多关注于依值类型编程。

本书最初的目标只是简单地改编《软件基础》，保持同样的内容，而只是将代码从 Coq 翻译成 Agda。但五年的课堂经验很快让我明白，自己有一些关于如何展示这些材料的想法。 有人说除非你不得不写书，否则绝对不要写书。而我很快发现这就是一本我不得不写的书。

我很幸运地得到了我的学生 Wen Kokke 的热情帮助。她引导着我站在 Agda 新手的视角写书，还提供了一些十分易用的工具来生成清晰易读的页面。

这里的大部分内容都是在 2018 年上半年的休假期间写的。

—— Philip Wadler，里约热内卢，2018 年 1 月 - 6 月

习题说明

标有推荐的习题是爱丁堡大学使用本教材的课程中学生需要做的。

标有延伸的习题提供了额外的挑战。很少有学生能全部做完，但至少应该尝试一下。

标有实践的习题供想要更多实践的学生练习。

你可以从 Github 上下载本书并将 “– 请将代码写在此处” 替换为你的习题解答。 此外，你也可能在课程作业中收到需要编辑的文件，其中包含了练习。

你在解题时或许需要导入库函数，也可能需要将 PLFA 设置为 Agda 库，方法可参考 读者指南。

请不要在公共空间中发表习题的答案。

GitHub 上有一个发布了部分习题答案的非公开代码仓库。如果你想获得访问，请联系 Philip Wadler。

使用说明

读者指南

《编程语言基础：Agda 语言描述》的使用方法与《Programming Language Foundations in Agda》一致。

本书可访问 PLFA-zh 在线阅读。

要参与翻译，请先阅读翻译规范。

你可以在线阅读 PLFA，无需安装任何东西。 然而，如果你想要交互式编写代码或完成习题，那么就需要几样东西：

• macOS 上：XCode 命令行工具
• Git
• GHC and Cabal
• Agda
• Agda 标准库
• PLFA

PLFA 只针对特定的 Agda 和 标准库版本进行了测试，相应版本已在前面的徽章中指明。 Agda 和标准库变化得十分迅速，而这些改变经常搞坏 PLFA，因此使用旧版或新版通常会出现问题。

Agda 和 Agda 标准库有多个版本。如果你使用了包管理器（如 Homebrew 或者 Debian apt），Agda 的版本可能不是最新的。除此之外，Agda 仍然在活跃的开发之中，如果你从 GitHub 上安装了开发版本，开发者的新变更也可能让这里的代码出现问题。 因此，使用上述版本的 Agda 和 Agda 标准库很重要。

macOS 平台：安装 XCode 命令行工具

在 macOS 平台，你需要安装 XCode 命令行工具。 在大多数 macOS 系统版本上，你可以用下面的命令安装它们：

xcode-select --install

安装 Git

你可以使用下面的命令来检查你是否安装了 Git。

git --version

如果你没有 Git，请参阅 Git 下载页面。

安装 GHC 和 Cabal

Agda 是用 Haskell 写成的，所以为了安装它我们需要 Glorious Haskell Compiler 和它的包管理器 Cabal。PLFA 应该在任何 >=8.10 的 GHC 版本下运行，在 8.10 到 9.8 版本下完成测试。我们建议使用 ghcup 来安装两者。 在 ghcup 安装好之后，输入下列命令：

ghcup install ghc 9.4.8
ghcup install cabal recommended

ghcup set ghc 9.4.8
ghcup set cabal recommended

或使用 ghcup tui 来『设置』合适的工具。

安装 Agda

安装 Agda 最简单的方法是通过 Cabal。PLFA 使用 Agda 版本 2.6.3。运行下面的命令：

cabal update
cabal install Agda-2.6.3

这一步会消耗很长时间和很多内存来完成。

如果你遇到了问题，或者想参考替代的方法，可参阅 Agda 安装指引。

如果你愿意，你可以测试 Agda 是否已正确安装。

安装 PLFA 和 Agda 标准库

我们建议您使用下面的命令把 PLFA 安装至你的家目录：

git clone --depth 1 --recurse-submodules --shallow-submodules https://github.com/plfa/plfa.github.io plfa

PLFA 包括了所需要的 Agda 标准库版本，如果你在克隆时使用了 --recurse-submodule 选项，你在 standard-library 文件夹中已经有了 Agda 标准库！

最后，我们需要让 Agda 知道如何找到标准库。 你需要两个配置文件，一个用于指定库的路径，一个用于指定默认载入的库。

在 macOS 和 Unix 上，如果 PLFA 已经安装至 Home 目录，且你没有希望保存的配置文件，运行下面的命令：

mkdir -p ~/.agda
cp ~/plfa/data/dotagda/* ~/.agda

这条命令提供了 Agda 标准库，也让 PLFA 可以当作一个 Agda 库来使用。

否则，你需要手动编辑相关的配置文件。两者都位于 AGDA_DIR 目录下。 在 UNIX 和 macOS 平台，AGDA_DIR 默认为 ~/.agda。在 Windows 平台，AGDA_DIR 一般默认为 %AppData%\agda，而 %AppData% 默认为 C:\Users\USERNAME\AppData\Roaming。

• 如果 AGDA_DIR 文件夹不存在，创建它。
• 在 AGDA_DIR 中，创建一个纯文本文件 libraries，内容为 /path/to/standard-library.agda-lib （即上文中记录的路径）。 这个文件让 Agda 知道有一个名为 standard-library 的库可用。
• 在 AGDA_DIR 中，创建一个纯文本文件 defaults，内容__仅__为 standard-library 这一行。
• 如果你想导入书中的模块，那么需要将 PLFA 设置为 Agda 库。假设 PLFA 是 PLFA 的根目录，完成此设置需要将 PLFA/src/plfa.agda-lib 作为单独的一行添加到 AGDA_DIR/libraries，并将 plfa 作为单独的一行添加到 AGDA_DIR/defaults。

关于放置标准库的更多信息可以参阅 Agda 文档中的库管理。

设置 Agda 的编辑器

Emacs

推荐的 Agda 编辑器是 Emacs。安装 Emacs 可以用下面的方法：

• UNIX：包管理器中的 Emacs 应该可以使用（只要它的版本比较新），GNU Emacs 下载页面也有最近发布版本的链接。
• MacOS：推荐的 Emacs 是 Aquamacs，但是 GNU Emacs 也可以通过 Homebrew 或者 MacPorts 安装。参阅 GNU Emacs 下载页面中的指示。
• Windows：参阅 GNU Emacs 下载页面中的指示。

确保你可以用你安装的版本打开、编辑、保存文件。GNU Emacs 网站上的 Emacs 向导描述了如果打开 Emacs 安装中的教程。

Agda 自带了 Emacs 编辑器支持，如果你安装了 Agda，运行下面的命令来配置 Emacs：

agda-mode setup
agda-mode compile

如果你已经是 Emacs 用户，并有自己的设置，你会发现 setup 命令向你的 .emacs 文件中追加了配置，来配合你已有的设置。

在 Emacs 中自动加载 agda-mode

从版本 2.6.0 开始，Agda 支持 Markdown 风格的文学编程，文件使用 .lagda.md 扩展名。 该扩展名的一个问题就是 Emacs 默认会进入 Markdown 编辑模式。 而为了让 agda-mode 在你打开 .agda 或 .lagda.md 文件时自动加载， 请将以下内容放到你的 Emacs 配置文件中：

;; auto-load agda-mode for .agda and .lagda.md
(setq auto-mode-alist
   (append
     '(("\\.agda\\'" . agda2-mode)
       ("\\.lagda.md\\'" . agda2-mode))
     auto-mode-alist))

如果你的配置中已有了改变 auto-mode-alist 的设置，将上述内容放置在已有的设置__之后__，或者将其与已有设置合并（如果你对 Emacs Lisp 足够了解）。 Emacs 的配置文件通常位于 ~/.emacs 或 ~/.emacs.d/init.el，然而 Aquamacs 用户需要将启动设置放到位于 ~/Library/Preferences/Aquamacs Emacs/Preferences 的 Preferences.el 文件中。 对于 Windows 平台，请参阅 GNU Emacs 文档 来寻找配置文件的位置。

可选：在 Emacs 中使用 Mononoki 字体

Agda 中的很多重要符号是用 Unicode 来表示的，因此用来显示和编辑 Agda 的字体需要正确地显示这些符号。最重要的是你使用的字体需要有好的 Unicode 字符支持。我们推荐 Mononoki， 其他的备选字体有 Source Code Pro、 DejaVu Sans Mono 和 FreeMono。

你可以直接从此网站 下载并安装 Mononoki。对于大多数系统来说，安装字体只是简单的下载 .otf 或者 .ttf 文件。 如果你的包管理器提供了 Mononoki 的包，那样可能更加简单。 例如，macOS 的 Homebrew 提供了 font-mononiki 包；Debian 的 APT 提供了 fonts-mononoki 包。 将下面的内容加入 Emacs 配置文件，可以把 Mononoki 设置为 Emacs 的默认字体：

;; default to mononoki
(set-face-attribute 'default nil
                    :family "mononoki"
                    :height 120
                    :weight 'normal
                    :width  'normal)

检查 agda-mode 是否正确安装

在 Emacs 中打开本书的第一章 (plfa/src/plfa/part1/Naturals.lagda.md)，输入 C-c C-l 来载入和类型检查这个文件。

在 Emacs 中使用 agda-mode

要加载文件并对其执行类型检查，请使用 C-c C-l。

Agda 的编辑是通过使用「洞」来交互的，它表示程序中尚未填充的片段。 如果用问号作为表达式，并用 C-c C-l 加载缓冲区，Agda 会将问号替换为一个「洞」。 当光标在洞中时，你可以做以下这些事情：

• C-c C-c: 分项（询问变量名，case）
• C-c C-空格：填洞
• C-c C-r：用构造子精化（refine）
• C-c C-a：自动填洞（automatic）
• C-c C-,：目标类型和语境
• C-c C-.：目标类型，语境，以及推断的类型

更多细节请见 emacs-mode 文档。

如果你想在 Agda 代码的侧边而非底栏查看信息，那么可以这样做：

• 打开 Agda 文件并按 C-c C-l；
• 按 C-x 1 来仅显示当前 Agda 文件；
• 按 C-x 3 来垂直分割窗口；
• 将光标移动到右侧窗口；
• 按 C-x b 并输入「Agda information」切换到该缓冲区。

现在，Agda 的错误消息将会在代码右侧显示，而非被挤压在底部的狭小空间里。

在 Emacs 中使用 agda-mode 输入 Unicode 字符

当你书写 Agda 代码时，你需要输入标准键盘上没有的字符。Emacs 的「Agda-mode」定义了字符翻译来让这件事更容易：当你输入特定普通字符的序列时，Emacs 会在 Agda 文件中使用对应的特殊字符来替换。

例如，我们可以在之前的 .agda 测试文件中加入一条注释。 比如说，我们想要加入下面的注释：

{- I am excited to type ∀ and → and ≤ and ≡ !! -}

前几个字符都是普通字符，我们可以如往常的方式输入它们……

{- I am excited to type

在最后一个空格之后，我们无法在键盘上找到 ∀ 这个键。这个字符的输入序列是四个字符 \all，所以我们输入这四个字符，当我们完成时，Emacs 会把它们替换成我们想要的……

{- I am excited to type ∀

我们继续输入其他字符。有时字符会在输入时发生变化，因为一个字符的输入序列是另一个字符输入序列的前缀。 在我们输入箭头时会出现这样的情况，它的输入序列是 \->。在输入 \- 之后我们会看到……

{- I am excited to type ∀ and -

……因为输入序列 \- 对应了一定长度的短横。当我们输入 > 时，­ 变成了 →！ ≤ 的输入序列是 \<=，≡ 的是 \==。

{- I am excited to type ∀ and → and ≤ and ≡

最后几个字符又回归了普通字符……

{- I am excited to type ∀ and → and ≤ and ≡ !! -}

如果你在 Emacs 中输入 Unicode 时遇到了问题，可以在每章的最后找到当前章节中用到的 Unicode 字符。

带有 agda-mode 的 Emacs 提供了很多有用的命令，其中有两个对处理 Unicode 字符时特别有用。 支持的字符的完整列表可使用 agda-input-show-translations 命令查看：

M-x agda-input-show-translations

agda-mode 支持的所有字符都会列出来。

如果你想知道如何在 agda 文件输入一个特定的 Unicode 字符，请将光标移动到该字符上并输入以下命令：

M-x quail-show-key

你会在迷你缓冲区中看到该字符对应的按键序列。

Spacemacs

Spacemacs 是一个「社区引领的 Emacs 版本」，对 Emacs 和 Vim 的编辑方式都有很好的支持。它自带集成了 agda-mode，所需的只是将 .spacemacs 中启用 Agda 支持。

Visual Studio Code

Visual Studio Code 是一个微软开发的开源代码编辑器。 Visual Studio 市场中有 Agda 插件。

Getting Started for Contributors

If you plan to build PLFA locally, please refer to Contributing for additional instructions.

Naturals: 自然数

module plfa.part1.Naturals where

夜空中的星星不计其数，但只有不到五千颗是肉眼可见的。 可观测宇宙中则包含大约 7*10^22 颗恒星。

星星虽多，但却是有限的，而自然数是无限的。就算用自然数把所有的星星都数尽了， 剩下的自然数也和开始的一样多。

自然数是一种归纳数据类型（Inductive Datatype）

大家都熟悉自然数，例如：

0
1
2
3
...

等等。我们将自然数的类型（Type）记作 ℕ ，并称 0、1、2、3 等数 是类型 ℕ 的值（Value），表示为 0 : ℕ，1 : ℕ，2 : ℕ，3 : ℕ 等等。

自然数集是无限的，然而其定义只需寥寥几行即可写出。下面是用两条推导规则（Inference Rules）定义的自然数：

--------
zero : ℕ

m : ℕ
---------
suc m : ℕ

以及用 Agda 定义的自然数：

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

其中 ℕ 是我们定义的数据类型（Datatype）的名字，而 zero（零）和 suc （后继，即 Successor 的简写）是该数据类型的构造子（Constructor）。

这两种定义说的是同一件事：

• 起始步骤（Base Case）：zero 是一个自然数。
• 归纳步骤（Inductive Case）：如果 m 是一个自然数，那么 suc m 也是。

此外，这两条规则给出了产生自然数唯一的方法。因此，可能的自然数包括：

zero
suc zero
suc (suc zero)
suc (suc (suc zero))
...

我们将 zero 简写为 0；将 suc zero，零的后继数， 也就是排在零之后的自然数，简写为 1；将 suc (suc zero)，也就是 suc 1， 即一的后继数，简写为 2；将二的后继数简写为 3；以此类推。

练习 seven（实践）

请写出 7 的完整定义。

-- 请将代码写在此处。

你需要为 seven 给出类型签名以及定义。在 Emacs 中使用 C-c C-l 来让 Agda 重新加载。

推导规则分析

我们来分析一下刚才的两条推导规则。每条推导规则包含写在一条水平直线上的 零条或多条判断（Judgment），称之为假设（Hypothesis）；以及写在 直线下的一条判断，称之为结论（Conclusion）。第一条规则是起始步骤：它没 有任何假设，其结论断言 zero 是一个自然数。第二条规则是归纳步骤：它有 一条假设，即 m 是自然数，而结论断言 suc m 也是一个自然数。

Agda 定义分析

现在分析一下 Agda 的定义。关键字 data 表示这是一个归纳定义， 也就是用构造子定义一个新的数据类型。

ℕ : Set

表示 ℕ 是新的数据类型的名字，它是一个 Set，也就是在 Agda 中对类型的称呼。 关键字 where 用于分隔数据类型的声明和构造子的声明。 每个构造子的声明独占一行，用缩进来指明它所属的 data 声明。

zero : ℕ
suc  : ℕ → ℕ

这两行给出了构造子 zero 和 suc 的类型签名（Signature）。 它们表示 zero 是一个自然数，suc 则取一个自然数作为参数，返回另一个自然数。

读者可能注意到 ℕ 和 → 在键盘上没有对应的按键。它们是 Unicode（统一码）中的符号。每一章的结尾都会有本章节引入的 Unicode 符号列表，以及在 Emacs 编辑器中输入它们的方法。

创世故事

我们再看一下自然数的定义规则：

• 起始步骤（Base Case）：zero 是一个自然数。
• 归纳步骤（Inductive Case）：如果 m 是一个自然数，那么 suc m 也是。

等等！第二行用自然数定义了自然数，这怎么能行？这个定义难道 不会像「脱欧即是脱欧」一样无用吗？

【译注：「脱欧即是脱欧」是英国首相特蕾莎·梅提出的一句口号。】

实际上，不必通过自我指涉，我们的自然数定义也是可以被赋予意义的。 我们甚至只需要处理有限的集合，而不必涉及无限的自然数集。

我们可以将这个过程比作一个创世故事。起初，我们对自然数一无所知：

-- 起初，世上没有自然数。

现在，我们对所有已知的自然数应用之前的规则。起始步骤告诉我们 zero 是 一个自然数，所以我们将它加入已知自然数的集合中。归纳步骤告诉我们如果 「昨天的」m 是一个自然数，那么「今天的」suc m 也是一个自然数。我们在 今天之前并不知道任何自然数，所以归纳步骤在此处不适用。

-- 第一天，世上有了一个自然数。
zero : ℕ

然后我们重复此过程。今天我们知道昨天的所有自然数，以及任何 通过规则添加的数。起始步骤依然告诉我们 zero 是一个自然数，我们 已经知道这件事了。而如今归纳步骤告诉我们，由于 zero 在昨天是自然数， 那么 suc zero 在今天也是自然数：

-- 第二天，世上有了两个自然数。
zero : ℕ
suc zero : ℕ

我们再次重复此过程。现在归纳步骤告诉我们，由于 zero 和 suc zero 都是自然 数，因此 suc zero 和 suc (suc zero) 也是自然数。我们已经知道 suc zero 是自然数了，而后者 suc (suc zero) 是新加入的。

-- 第三天，世上有了三个自然数。
zero : ℕ
suc zero : ℕ
suc (suc zero) : ℕ

此时规律已经很明显了。

-- 第四天，世上有了四个自然数。
zero : ℕ
suc zero : ℕ
suc (suc zero) : ℕ
suc (suc (suc zero)) : ℕ

此过程可以继续下去。在第 n 天会有 n 个不同的自然数。每个自然数都会在 某一天出现。具体来说，自然数 n 在第 n+1 天首次出现。至此，我们并没有使 用自然数集来定义其自身，而是根据第 n 天的数集定义了第 n+1 天的数集。

像这样的过程被称作是归纳的（Inductive）。我们从一无所有开始，通过应用将 一个有限集合转换到另一个有限集合的规则，逐步生成潜在无限的集合。

定义了零的规则之所以被称作起始步骤，是因为它在我们还不知道其它自然数时 就引入了一个自然数。定义了后继数的规则之所以被称作归纳步骤，则是因为它在 已知自然数的基础上引入了更多自然数。其中，起始步骤的重要性不可小觑。如果 只有归纳步骤，那么第一天就没有任何自然数。第二天，第三天，无论多久也依旧没有。 一个没有起始步骤的归纳定义是无用的，就像「脱欧即是脱欧」一样。

哲学和历史

哲学家发现，我们对「第一天」「第二天」等说法的使用暗含了对自然数的理解。 在这个层面上，我们对自然数的定义也许某种程度上可以说是循环的，但我们不必为此烦恼。 每个人对自然数都有良好的非形式化的理解，而我们可以将它作为形式化描述自然数的基础。

尽管从人类开始计数起，自然数就被人所认知，然而其归纳定义却是近代的事情。 这可以追溯到理查德·戴德金（Richard Dedekind）于 1888 年发表的论文 Was sind und was sollen die Zahlen?”（《数是什么，应该是什么？》）， 以及朱塞佩·皮亚诺（Giuseppe Peano）于次年发表的著作 “Arithmetices principia, nova methodo exposita”（《算术原理：用一种新方法呈现》）。

编译指令

在 Agda 中，任何跟在 -- 之后或者由 {- 和 -} 包裹的文字都会被视为 注释（Comment）。一般的注释对代码没有任何作用，但有一种例外， 这种注释被称作编译指令（Pragma），由 {-# 和 #-} 包裹。

{-# BUILTIN NATURAL ℕ #-}

这一行告诉 Agda 数据类型 ℕ 对应了自然数，然后编写者就可以将 zero 简写 为 0，将 suc zero 简写为 1，将 suc (suc zero) 简写为 2 了，以此类推。 必须要向编译指令给出之前声明的类型（本例中为 ℕ），该类型有且只有两个构造子， 其中一个没有参数（本例中为 zero），另一个只接受一个所给定类型的参数（本例中为 suc）。

在启用上述简写的同时，这条编译指令也会用 Haskell 的任意精度整数类型 来提供更高效的自然数内部表示。用 zero 和 suc 表示自然数 n 要占用正比 于 n 的空间，而将其表示为 Haskell 中的任意精度整数只会占用正比于 n 的对数的空间。

导入模块

我们很快就能写一些包含自然数的等式了。在此之前，我们需要从 Agda 标准库 中导入相等性（Equality）的定义和用于等式推理的记法：

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

第一行代码将标准库中定义了相等性的模块导入到当前作用域（Scope）中， 并将其命名为 Eq。第二行打开了这个模块，也就是将所有在 using 从句中指定的名称添加到当前作用域中。此处添加的名称有相等性运算符 _≡_ 和两个项相等的证据 refl。第三行选取的模块提供了用于等价关系推理的运算符，并将 using 从句中指定的名称添加到当前作用域。此处添加的名称有 begin_、 _≡⟨⟩_ 和 _∎。我们后面会看到这些运算符的使用方法。现在暂且把它们当作现成的 工具来使用，不深究其细节。但我们会在相等性一章中 学习它们的具体定义。

Agda 用下划线来标注项（Term）在中缀（Infix）或混缀（Mixfix）运算符中项出现的位置。 因此，_≡_ 和 _≡⟨⟩_ 是中缀的（运算符写在两个项之间），而 begin_ 是前缀的 （运算符写在项之前），_∎ 则是后缀的（运算符写在项之后）。

括号和分号是少有的几个不能在名称中出现的的字符，于是我们在 using 列表中不需要额外的空格来消除歧义。

自然数的运算是递归函数

既然我们有了自然数，那么可以用它们做什么呢？比如，我们能定义 加法和乘法之类的算术运算吗？

我儿时曾花费了大量的时间来记忆加法表和乘法表。最开始，运算规则看起来很 复杂，我也经常犯错。在发现递归（Recursion）时，我如同醍醐灌顶。 有了这种简单的技巧，无数的加法和乘法运算只用几行就能概括。

这是用 Agda 编写的加法定义：

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

我们来分析一下它的定义。加法是一种中缀运算符，其名为 _+_，其中参数的 位置用下划线表示。第一行指定了运算符的类型签名。类型 ℕ → ℕ → ℕ 表示 加法接受两个自然数作为参数，并返回一个自然数。中缀记法只是函数应用的简写， m + n 和 _+_ m n 这两个项是等价的。

它的定义包含一个起始步骤和一个归纳步骤，与自然数的定义对应。起始步骤说明 零加上一个数仍返回这个数，即 zero + n 等于 n。归纳步骤说明一个数的后继数 加上另一个数返回两数之和的后继数，即 (suc m) + n 等于 suc (m + n)。在加法的 定义中，构造子出现在了等式左边，我们称之为模式匹配（Pattern Matching）。

如果我们将 zero 写作 0，将 suc m 写作 1 + m，上面的定义就变成了 两个熟悉的等式。

 0       + n  ≡  n
 (1 + m) + n  ≡  1 + (m + n)

因为零是加法的幺元，所以第一个等式成立。又因为加法满足结合律，所以 第二个等式也成立。加法结合律的一般形式如下，说明运算结果与括号位置无关。

 (m + n) + p  ≡  m + (n + p)

将上面第三个等式中的 m 换成 1，n 换成 m，p 换成 n，我们就 得到了第二个等式。我们用等号 = 表示定义，用 ≡ 断言两个已定义的事物相等。

加法的定义是递归（Recursive）的，因为在最后一行我们用加法定义了加法。 与自然数的归纳定义类似，这种表面上的循环性并不会造成问题，因为较大 的数相加是用较小的数相加定义的。这样的定义被称作是良基的（Well founded）。

例如，我们来计算二加三：

_ :  +  ≡ 
_ =
  begin
     + 
  ≡⟨⟩    -- 展开为
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- 归纳步骤
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩    -- 归纳步骤
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩    -- 起始步骤
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩    -- 简写为
    
  ∎

我们可以按需展开简写，把同样的推导过程写得更加紧凑。

_ :  +  ≡ 
_ =
  begin
     + 
  ≡⟨⟩
    suc ( + )
  ≡⟨⟩
    suc (suc ( + ))
  ≡⟨⟩
    suc (suc )
  ≡⟨⟩
    
  ∎

第一行取 m = 1 和 n = 3 匹配了归纳步骤，第二行取 m = 0 和 n = 3 匹配了归纳步骤，第三行取 n = 3 匹配了起始步骤。

以上两个推导过程都由一个类型签名（包含冒号 : 的一行）和一个提供对应类型 的项的绑定（Binding）（包含等号 = 的一行及之后的部分）组成。在编写代码时 我们用了虚设名称 _。虚设名称可以被重复使用，在举例时非常方便。除了 _ 之外 的名称在一个模块里只能被定义一次。

这里的类型是 2 + 3 ≡ 5，而该等式写成列表形式的等式链的项，提供了类型中表示 等式成立的证据（Evidence）。该等式链由 begin 开始，以 ∎ 结束（∎ 可读作「qed（证毕）」或「tombstone（墓碑符号）」，后者来自于其外观）， 并由一系列 ≡⟨⟩ 分隔的项组成。

注意，上面的证明以彩色显示，表示 Agda 已经处理并接受了这些代码， 因此可以保证它们没有类型错误。在 Agda 中处理后，Emacs 源文件中会以同样的颜色显示。 在 Emacs 中，右键单击任何彩色的符号，例如 +、suc 或 ≡，就会跳转到该符号的定义。

其实，以上两种证明都比实际所需的要长，下面的证明就足以让 Agda 满意了。

_ :  +  ≡ 
_ = refl

Agda 知道如何计算 2 + 3 的值，也可以立刻确定这个值和 5 是一样的。如果一个 二元关系（Binary Relation）中每个值都和自己相关，我们称这个二元关系满足 自反性（Reflexivity）。在 Agda 中，一个值等于其自身的证据写作 refl。

在等式链中，Agda 只检查每个项是否都能化简为相同的值。如果我们打乱等式顺序， 省略或者加入一些额外的步骤，证明仍然会被接受。我们需要自己来保证等式的顺序 便于理解。

在这里，2 + 3 ≡ 5 是一个类型，等式链（以及 refl）都是这个类型的项。 换言之，我们也可以把每个项都看作断言 2 + 3 ≡ 5 的证据。这种解释的 对偶性——类型即命题，项即证据——是我们在 Agda 中形式化各种概念的核心， 也是贯穿本书的主题。

注意，当我们使用证据这个词时不容一点含糊。这里的证据确凿不移， 不像法庭上的证词一样必须被反复权衡以决定证人是否可信。 我们也会使用证明一词表达相同的意思，在本书中这两个词可以互换使用。

练习 +-example（实践）

计算 3 + 4，将你的推导过程写成等式链，为 + 使用等式。

-- 请将代码写在此处。

乘法

一旦我们定义了加法，我们就可以将乘法定义为重复的加法。

_*_ : ℕ → ℕ → ℕ
zero    * n  =  zero
(suc m) * n  =  n + (m * n)

计算 m * n 返回的结果是 m 个 n 之和。

重写定义再一次给出了两个熟悉的等式：

0       * n  ≡  0
(1 + m) * n  ≡  n + (m * n)

因为零乘任何数都是零，所以第一个等式成立。因为乘法对加法有分配律，所以 第二个等式也成立。乘法对加法的分配律的一般形式如下：

(m + n) * p  ≡  (m * p) + (n * p)

将上面第三个等式中的 m 换成 1，n 换成 m，p 换成 n，再根据 一是乘法的幺元，也就是 1 * n ≡ n，我们就得到了第二个等式。

这个定义也是良基的，因为较大的数相乘是用较小的数相乘定义的。

例如，我们来计算二乘三：

_ =
  begin
     * 
  ≡⟨⟩    -- 归纳步骤
     + ( * )
  ≡⟨⟩    -- 归纳步骤
     + ( + ( * ))
  ≡⟨⟩    -- 起始步骤
     + ( + )
  ≡⟨⟩    -- 化简
    
  ∎

第一行取 m = 1 和 n = 3 匹配了归纳步骤，第二行取 m = 0 和 n = 3 匹配了归纳步骤，最后第三行取 n = 3 匹配了起始步骤。在这里我们省略了 _ : 2 * 3 ≡ 6 的签名，因为它很容易从对应的项推导出来。

练习 *-example（实践）

计算 3 * 4，将你的推导过程写成等式链，为 * 使用等式。 （不必写出 + 求值的每一步。）

-- 请将代码写在此处。

练习 _^_（推荐）

根据以下等式写出乘方的定义。

m ^ 0        =  1
m ^ (1 + n)  =  m * (m ^ n)

检查 3 ^ 4 是否等于 81。

-- 请将代码写在此处。

饱和减法

我们也可以定义减法。由于没有负的自然数，如果被减数比减数小， 我们就将结果取零。这种针对自然数的减法变种称作饱和减法（Monus，由 minus 修改而来）。

饱和减法是我们首次在定义中对两个参数都使用模式匹配：

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

我们可以通过简单的分析来说明所有的情况都被考虑了。

• 考虑第二个参数。
  • 如果它是 zero，应用第一个等式。
  • 如果它是 suc n，考虑第一个参数。
    • 如果它是 zero，应用第二个等式。
    • 如果它是 suc m，应用第三个等式。

Agda will raise an error if all the cases are not covered. As with addition and multiplication, the recursive definition is well founded because monus on bigger numbers is defined in terms of monus on smaller numbers.

例如，我们来计算三减二：

_ =
  begin
     ∸ 
  ≡⟨⟩
     ∸ 
  ≡⟨⟩
     ∸ 
  ≡⟨⟩
    
  ∎

我们没有使用第二个等式，但是如果被减数比减数小，我们还是会用到它。

_ =
  begin
     ∸ 
  ≡⟨⟩
     ∸ 
  ≡⟨⟩
     ∸ 
  ≡⟨⟩
    
  ∎

我们对饱和减法的定义确保了只有一条等式可以应用。 假设我们将第二条以下文取而代之

zero  ∸ n  =  zero

那样就不清楚 Agda 应该使用第一条或者第二条来简化 zero ∸ zero。 在这样的情况下，两者都可以相同的答案 zero，但这不一定是普遍的情况。 将

{-# OPTIONS --exact-split #-}

写在文件的开始可以让 Agda 在不同情况相互重叠时产生一个错误， 有些时候这会有帮助。我们会在逻辑连接符部分 展示一个这样的例子。

练习 ∸-example₁ 和 ∸-example₂（推荐）

计算 5 ∸ 3 和 3 ∸ 5，将你的推导过程写成等式链。

-- 请将代码写在此处。

优先级

我们经常使用优先级（Precedence）来避免书写大量的括号。 函数应用比其它任何运算符都结合得更紧密（即有更高的优先级），所以我们 可以用 suc m + n 来表示 (suc m) + n。另一个例子是，我们说乘法比 加法结合得更紧密，所以可以用 n + m * n 来表示 n + (m * n)。我们有 时候也说加法是左结合的，所以可以用 m + n + p 来表示 (m + n) + p。

在 Agda 中，中缀运算符的优先级和结合性需要被声明：

infixl   _+_  _∸_
infixl   _*_

它声明了运算符 _+_ 和 _∸_ 的优先级为 6，运算符 _*_ 的优先级 为 7。因为加法和饱和减法的优先级更低，所以它们结合得不如乘法紧密。 infixl 意味着三个运算符都是左结合的。编写者也可以用 infixr 来表示 某个运算符是右结合的，或者用 infix 来表示总是需要括号来消除歧义。

柯里化

我们曾将接受两个参数的函数表示成「接受第一个参数，返回接受第二个 参数的函数」的函数。这种技巧叫做柯里化（Currying）。

与 Haskell 和 ML 等函数式语言类似，Agda 在设计时就考虑了让柯里化更加易用。 函数箭头是右结合的，而函数应用是左结合的。

比如

ℕ → ℕ → ℕ 表示 ℕ → (ℕ → ℕ)

而

_+_ 2 3 表示 (_+_ 2) 3。

_+_ 2 这个项表示一个「将参数加二」的函数，因此将它应用到三就得到了五。

柯里化是以哈斯凯尔·柯里（Haskell Curry）的名字命名的，编程语言 Haskell 也是。 柯里的工作可以追溯到 19 世纪 30 年代。当我第一次了解到柯里化时， 有人告诉我柯里化的命名是个归因错误，因为在 20 年代同样的想法就已经被 Moses Schönfinkel 提出了。我也听说过这样一个笑话：「（柯里化）本来该命名成 Schönfinkel 化的，但是咖喱（Curry）更好吃」。直到之后我才了解到， 这个归因错误的解释本身也是个归因错误。柯里化的概念早在戈特洛布·弗雷格 （Gottlob Frege）发表于 1879 年的 “Begriffsschrift”（《概念文字》）中就出现了。

又一个创世故事

和归纳定义中用自然数定义了自然数一样，递归定义也用加法定义了加法。

同理，无需利用循环性，我们的加法定义也是可以被赋予意义的。 为此，我们需要将加法的定义规约到用于判断相等性的等价的推导规则上来。

n : ℕ
--------------
zero + n  =  n

m + n  =  p
---------------------
(suc m) + n  =  suc p

假设我们已经定义了自然数的无限集合，指定了判断 n : ℕ 的意义。 第一条推导规则是起始步骤。它断言如果 n 是一个自然数，那么零加上它得 n。 第二条推导规则是归纳步骤。它断言如果 m 加上 n 得 p，那么 suc m 加 上 n 得 suc p。

我们同样借创世故事来帮助理解，不过这次关注的是关于加法的判断。

-- 起初，我们对加法一无所知。

现在对所有已知的判断应用之前的规则。起始步骤告诉我们，对于 每个自然数 n 都有 zero + n = n，因此我们添加所有的这类等式。 归纳步骤告诉我们，如果「昨天」有 m + n = p，那么「今天」 就有 suc m + n = suc p。在今天之前，我们不知道任何关于加法的等式， 因此这条规则不会给我们任何新的等式。

-- 第一天，我们知道了 0 为被加数的加法。
0 + 0 = 0     0 + 1 = 1    0 + 2 = 2     ...

然后我们重复这个过程。今天我们知道来自昨天的所有等式，以及任何通过 规则添加的等式。起始步骤没有告诉我们任何新东西，但是归纳步骤添加了更多的等式。

-- 第二天，我们知道了 0，1 为被加数的加法。
0 + 0 = 0     0 + 1 = 1     0 + 2 = 2     0 + 3 = 3     ...
1 + 0 = 1     1 + 1 = 2     1 + 2 = 3     1 + 3 = 4     ...

我们再次重复这个过程：

-- 第三天，我们知道了 0，1，2 为被加数的加法。
0 + 0 = 0     0 + 1 = 1     0 + 2 = 2     0 + 3 = 3     ...
1 + 0 = 1     1 + 1 = 2     1 + 2 = 3     1 + 3 = 4     ...
2 + 0 = 2     2 + 1 = 3     2 + 2 = 4     2 + 3 = 5     ...

此时规律已经很明显了：

-- 第四天，我们知道了 0，1，2，3 为被加数的加法。
0 + 0 = 0     0 + 1 = 1     0 + 2 = 2     0 + 3 = 3     ...
1 + 0 = 1     1 + 1 = 2     1 + 2 = 3     1 + 3 = 4     ...
2 + 0 = 2     2 + 1 = 3     2 + 2 = 4     2 + 3 = 5     ...
3 + 0 = 3     3 + 1 = 4     3 + 2 = 5     3 + 3 = 6     ...

此过程可以继续下去。在第 m 天我们将知道所有被加数小于 m 的等式。

如上所示，归纳定义和递归定义的的推导过程十分相似。它们就像一枚硬币的两面。

有限的创世故事

前面的创世故事是用分层的方式讲述的。首先，我们创造了自然数的无限集合。 然后，我们构造加法的实例时把自然数集视为现成的，所以即使在第一天我 们也有一个无限的实例集合。

然而，我们也可以选择同时构造自然数集和加法的实例。这样在任何一天都只会有 一个有限的实例集合。

-- 起初，我们一无所知。

现在，对我们已知的所有判断应用之前的规则。只有自然数的起始步骤适用：

-- 第一天，我们知道了零。
0 : ℕ

我们再次应用所有的规则。这次我们有了一个新自然数，和加法的第一个等式。

-- 第二天，我们知道了一和所有和为零的加法算式。
0 : ℕ
1 : ℕ    0 + 0 = 0

然后我们重复这个过程。我们通过加法的起始步骤得到了一个等式，也通过在前一天 的等式上应用加法的归纳步骤得到了一个等式：

-- 第三天，我们知道了二和所有和为一的加法算式。
0 : ℕ
1 : ℕ    0 + 0 = 0
2 : ℕ    0 + 1 = 1   1 + 0 = 1

此时规律已经很明显了：

-- 第四天，我们知道了三和所有和为二的加法算式。
0 : ℕ
1 : ℕ    0 + 0 = 0
2 : ℕ    0 + 1 = 1   1 + 0 = 1
3 : ℕ    0 + 2 = 2   1 + 1 = 2    2 + 0 = 2

在第 n 天会有 n 个不同的自然数和 n × (n-1) / 2 个加法等式。 数字 n 和所有和小于 n 的加法等式在第 n+1 天首次出现。这提供了 一种无限的数据集合及与之相关的等式的有限主义视角。

交互式地编写定义

Agda 被设计为使用 Emacs 作为文本编辑器，二者一同提供了很多能帮助 用户交互式地创建定义和证明的功能。

我们从输入以下代码开始：

_+_ : ℕ → ℕ → ℕ
m + n = ?

问号表示你希望 Agda 帮助你填入这部分代码。如果按下组合键 C-c C-l （按住 Control 键的同时先按 c 键再按 l 键，l 键代表载入 load），这个问号会被替换：

_+_ : ℕ → ℕ → ℕ
m + n = { }0

这对花括号被称作一个洞（Hole），0 是这个洞的编号。洞将会被高亮显示为 绿色（或蓝色）。同时，Emacs 会创建一个窗口显示如下文字：

?0 : ℕ

这表示 0 号洞需要填入一个类型为 ℕ 的项。按组合键 C-c C-f （f 键代表向前 forward）会移动到下一个洞。

我们希望在第一个参数上递归来定义加法。 将光标移至 0 号洞并按 C-c C-c（c 键代表分情况讨论 case），你将看见如下提示：

pattern variables to case (empty for split on result):

即「用于分项的模式变量（留空以对结果分项）：」。

键入 m 会对名为 m 的变量分项（即自动模式匹配），并将代码更新为：

_+_ : ℕ → ℕ → ℕ
zero + n = { }0
suc m + n = { }1

现在有两个洞了。底部的窗口会告诉你每个洞所需的类型：

?0 : ℕ
?1 : ℕ

移动至 0 号洞，按下 C-c C-, 会显示当前洞所需类型的具体信息，以及 可用的自由变量：

Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ

这些信息强烈建议了用 n 填入该洞。填入内容后，你可以按下 C-c C-空格 来移除这个洞。

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = { }1

同理，移动到 1 号洞并按下 C-c C-, 会显示当前洞所需类型的具体信息， 以及可用的自由变量：

Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ
m : ℕ

移动到一个洞并按下 C-c C-r （r 键表示细分 refine）会将一个构造子填入这个洞（如果有唯一的选择的话）， 或者告诉你有哪些可用的构造子以供选择。在当前情况下，编辑器会显示如下内容：

Don't know which constructor to introduce of zero or suc

即「不知道在 zero 和 suc 中该引入哪一个构造子」。

我们将 suc ? 填入并按下 C-c C-空格，它会将代码更新为：

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc { }1

移动到新的洞并按下 C-c C-, 给出了和之前类似的信息：

Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ
m : ℕ

我们可以用 m + n 填入该洞并按 C-c C-空格 来完成程序：

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

在如此简单的程序上频繁使用交互操作可能帮助不大， 但是同样的技巧能够帮助你构建更复杂的程序。甚至对于加法定义这么简单的程序，使用 C-c C-c 来分项仍然是有用的。

更多编译指令

{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _∸_ #-}

以上几行告诉 Agda 这几个运算符和数学中常用的运算符相对应， 以便让它在计算时使用相应的，可处理任意精度整数类型的 Haskell 运算符。 计算 m 加 n 时，用 zero 和 suc 表示的自然数需要正比于 m 的时间， 而用 Haskell 整数表示的情况下只需要正比于 m 和 n 中较大者的对数的时间。 类似地，计算 m 乘 n 时，用 zero 和 suc 表示的自然数需要正比于 m 乘 n 的 时间，而用 Haskell 整数表示的情况下只需要正比于 m 和 n 的对数之和的时间。

练习 Bin（拓展）

使用二进制系统能提供比一进制系统更高效的自然数表示。我们可以用一个比特串来表示一个数：

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

例如，以下比特串

1011

代表数字十一被编码为了

⟨⟩ I O I I

由于前导零的存在，表示并不是唯一的。因此，十一同样可以 表示成 001011，编码为：

⟨⟩ O O I O I I

定义这样一个函数

inc : Bin → Bin

将一个比特串转换成下一个数的比特串。比如，1100 编码了十二，我们就应该有：

inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O

实现这个函数，并验证它对于表示零到四的比特串都能给出正确结果。

使用以上的定义，再定义一对函数用于在两种表示间转换。

to   : ℕ → Bin
from : Bin → ℕ

对于前者，用没有前导零的比特串来表示正数，并用 ⟨⟩ O 表示零。 验证这两个函数都能对零到四给出正确结果。

-- 请将代码写在此处。

标准库

在每一章的结尾，我们将展示如何在标准库中找到相关的定义。 自然数，它们的构造子，以及用于自然数的基本运算符，都在标准库模块 Data.Nat 中定义：

-- import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)

正常情况下，我们会以运行代码的形式展示一个导入语句， 这样如果我们尝试导入一个不可用的定义，Agda 就会报错。 不过现在，我们只在注释里展示了这个导入语句。这一章和标准库 都调用了 NATURAL 编译指令。我们是在 ℕ 上使用，而标准库是在 等价的类型 Data.Nat.ℕ 上使用。这样的编译指令只能被调用一次，因为 重复调用会导致 2 到底是类型 ℕ 的值还是类型 Data.Nat.ℕ 的 值这样的困惑。重复调用其它的编译指令也会导致同样的问题。基于这个原因， 我们在后续章节中通常会避免使用编译指令。更多关于编译指令的信息可在 Agda 文档中找到。

Unicode

这一章使用了如下的 Unicode 符号：

ℕ  U+2115  双线体大写 N (\bN)
→  U+2192  右箭头 (\to, \r, \->)
∸  U+2238  点减 (\.-)
≡  U+2261  等价于 (\==)
⟨  U+27E8  数学左尖括号 (\<)
⟩  U+27E9  数学右尖括号 (\>)
∎  U+220E  证毕 (\qed)

以上的每一行均包含 Unicode 符号（如 ℕ），对应的 Unicode 码点（如 U+2115）， 符号的名称（如 双线体大写 N），以及用于在 Emacs 中键入该符号的按键序列（如 \bN）。

通过 \r 命令可以查看多种右箭头符号。在输入 \r 后，你可以 按左、右、上、下键来查看或选择可用的箭头符号。这个命令会记住你上一次选择的位置， 并在下一次使用时从该字符开始。用于输入左箭头的 \l 命令的用法与此类似。

除了在输入箭头的命令中使用左、右、上、下键以外，以下按键也可以起到相同的作用：

C-b  左（后退一个字符）
C-f  右（前进一个字符）
C-p  上（到上一行）
C-n  下（到下一行）

C-b 表示按 Control + b，其余同理。你也可以直接输入显示的列表中的数字编号来选择。

要查看所支持字符的完整列表，请执行 agda-input-show-translations 命令：

M-x agda-input-show-translations

这样会显示出 agda-mode 中所有支持的字符。我们用 M-x 表示按下 ESC 后再按下 x。

如果你想知道如何在 agda 文件中输入一个特定的 Unicode 字符，请将光标移至该字符上， 然后执行 quail-show-key 命令：

M-x quail-show-key

你会在迷你缓冲区中看到输入该字符所需的按键序列。 例如，如果你在 ∸ 上执行 M-x quail-show-key，就会看到该字符的按键序列为 \.-。

Induction: 归纳证明

module plfa.part1.Induction where

归纳会让你对无中生有感到内疚 ……但它却是文明中最伟大的思想之一。 —— Herbert Wilf

现在我们定义了自然数及其运算，下一步是学习如何证明它们满足的性质。 顾名思义，归纳数据类型（Inductive Datatype）是通过归纳（Induction） 来证明的。

导入

我们需要上一章中的相等性，加上自然数及其运算。我们还导入了一些新的运算： cong、sym 和 _≡⟨_⟩_，之后会解释它们：

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_;_^_)

(Importing step-≡ defines _≡⟨_⟩_.)

运算符的性质

运算符随处可见，而数学家们统一了一些最常见的性质的名称。

• 幺元（Identity）：对于所有的 n，若 0 + n ≡ n，则 + 有左幺元 0； 若 n + 0 ≡ n，则 + 有右幺元 0。同时为左幺元和右幺元的值称简称幺元。 幺元有时也称作单位元（Unit）。

• 结合律（Associativity）：若括号的位置无关紧要，则称运算符 + 满足结合律， 即对于所有的 m、n 和 p，有 (m + n) + p ≡ m + (n + p)。

• 交换律（Commutativity）：若参数的顺序无关紧要，则称运算符 + 满足交换律， 即对于所有的 m 和 n，有 m + n ≡ n + m。

• 分配律（Distributivity）：对于所有的 m、n 和 p，若 m * (p + q) ≡ (m * p) + (m * q)，则运算符 * 对运算符 + 满足左分配律； 对于所有的 m、n 和 p，若 (m + n) * p ≡ (m * p) + (n * p)，则满足右分配律。

加法的幺元为 0，乘法的幺元为 1。加法和乘法都满足结合律和交换律， 乘法对加法满足分配律。

如果你在一个舞会上碰见了一位操作员，那么你可以跟他闲聊，问问他是否有单位元， 能不能结合或者交换。如果你碰见了两位操作员，那么可以问他们某一位是否在另一位上面分布。

【译注：作者的双关冷笑话，运算符（Operator）也有操作员的意思。】

正经来说，如果你在阅读技术论文时遇到了一个运算符，那么你可以考察它是否拥有幺元， 是否满足结合律或分配律，或者是否对另一个运算符满足分配律，这能为你提供一种视角。 细心的作者通常会指出它们是否满足这些性质，比如说指明一个新引入的运算符满足结合律 但不满足交换律。

练习 operators（实践）

请给出另一对运算符，它们拥有一个幺元，满足结合律、交换律，且其中一个对另一个满足分配律。 （你不必证明这些性质）

-- 请将代码写在此处。

请给出一个运算符的例子，它拥有幺元、满足结合律但不满足交换律。 （你不必证明这些性质）

-- 请将代码写在此处。

结合律

加法的一个性质是满足结合律，即括号的位置无关紧要：

(m + n) + p ≡ m + (n + p)

这里的变量 m、n 和 p 的取值范围都是全体自然数。

我们可以为这三个变量选取特定的数值来验证此命题：

_ : ( + ) +  ≡  + ( + )
_ =
  begin
    ( + ) + 
  ≡⟨⟩
     + 
  ≡⟨⟩
    
  ≡⟨⟩
     + 
  ≡⟨⟩
     + ( + )
  ∎

在这里，我们将计算过程写成了等式链，每行一个式子。这样的等式链通常非常易读， 你可以从上到下，直到遇到最简形式（本例中为 12），也可以从下到上，直到回到同样的式子。

该测试揭示了结合律可能没有它初看起来那么显然。为什么 7 + 5 与 3 + 9 相同？ 我们可能需要收集更多证据，选择其它的数值来验证此命题。但由于自然数是无限的， 因此测试永远无法完成。那么我们还有其它可以确保结合律对于所有自然数都成立的方法吗？

当然有！我们可以用归纳证明（Proof by Induction） 来确保某个性质对于所有的自然数都成立。

归纳证明

回想自然数的定义，它由一个起始步骤「zero 是一个自然数」 和一个归纳步骤「若 m 是一个自然数，则 suc m 也是一个自然数」构成。

归纳证明遵循此定义的结构。要通过归纳证明自然数的某个性质，我们需要两个步骤。 其一是起始步骤，即需要证明此性质对 zero 成立。其二是归纳步骤， 即假设此性质对一个任意自然数 m 成立（我们称之为归纳假设（Induction Hypothesis）），然后证明该性质对 suc m 必定成立。

若将 m 的某种性质（Property）写作 P m，那么我们需要证明的就是以下两个推导规则：

------
P zero

P m
---------
P (suc m)

先来分析一下这些规则。第一条规则是起始步骤，它需要我们证明性质 P 对 zero 成立。第二条规则是归纳步骤，它需要我们证明若归纳假设「P 对 m 成立」， 那么 P 也对 suc m 成立。

为什么可以这样做呢？它也可以用创世故事来讲解。起初，我们对性质一无所知：

-- 起初，世上没有已知的性质。

现在我们对所有已知的性质应用上述两条规则。起始步骤告诉我们 P zero 成立， 所以我们将它加入已知的性质集合中。归纳步骤告诉我们若「昨天的」P m 成立， 那么「今天的」P (suc m) 也成立。我们在今天之前并不知道任何性质， 因此归纳步骤在这里不适用：

-- 第一天，我们知道了一个性质。
P zero

然后我们重复此过程。在接下来的一天我们知道今天之前的所有性质， 以及任何通过此规则添加的性质。起始步骤告诉我们 P zero 成立，我们已经知道这件事了。而如今归纳步骤告诉我们，由于 P zero 在昨天成立，那么 P (suc zero) 今天也成立。

-- 第二天，我们知道了两个性质。
P zero
P (suc zero)

我们再重复此过程。现在归纳步骤告诉我们由于 P zero 和 P (suc zero) 都成立， 因此 P (suc zero) 和 P (suc (suc zero)) 也成立。我们已经知道第一个成立了， 但第二个是新引入的：

-- 第三天，我们知道了三个性质。
P zero
P (suc zero)
P (suc (suc zero))

此时规律已经很明显了：

-- 第四天，我们知道了四个性质。
P zero
P (suc zero)
P (suc (suc zero))
P (suc (suc (suc zero)))

此过程可以继续下去。在第 n 天会有 n 个不同的性质成立。 每个自然数的性质都会在某一天出现。具体来说，性质 P n 会在第 n+1 天 首次出现。

第一个证明：结合律

要证明结合律，我们需要将 P m 看做以下性质：

(m + n) + p ≡ m + (n + p)

这里的 n 和 p 是任意自然数，因此若我们可以证明该等式对所有的 m 都成立，那么它也会对所有的 n 和 p 成立。其推理规则的对应实例如下：

-------------------------------
(zero + n) + p ≡ zero + (n + p)

(m + n) + p ≡ m + (n + p)
---------------------------------
(suc m + n) + p ≡ suc m + (n + p)

如果我们可以证明这两条规则，那么加法结合律就可以用归纳法来证明。

以下为此性质的陈述和证明：

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎

我们将此证明命名为 +-assoc。在 Agda 中，标识符可以由除空格和 @.(){};_ 之外的任何字符序列构成。

我们来分析一下这段代码。其签名（Signature）描述了我们定义的标识符 +-assoc 为以下命题提供了证据（Evidence）：

∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

倒 A 符号读作「对于所有（for all）」，而该命题断言对于所有的自然数 m、n 和 p，等式 (m + n) + p ≡ m + (n + p) 成立。该命题的证据是一个接受三个自然数的函数， 将它们绑定到 m、n 和 p，并返回该等式对应实例的证据。

对于起始步骤，我们必须证明：

(zero + n) + p ≡ zero + (n + p)

用加法的起始步骤化简等式两边会得到：

n + p ≡ n + p

此式平凡成立。阅读此证明中起始步骤中的等式链，其最初和最末的式子分别匹配待证等式的两边， 从上到下或从下到上读都会让我们在中间遇到 n + p 。此步骤无需多言，化简即可。

对于归纳步骤，我们必须证明：

(suc m + n) + p ≡ suc m + (n + p)

用加法的归纳步骤化简等式两边会得到：

suc ((m + n) + p) ≡ suc (m + (n + p))

反之，它也可以通过在归纳假设

(m + n) + p ≡ m + (n + p)

两边之前加上 suc 得到。

阅读此证明中归纳步骤的等式链，其最初和最末的式子分别匹配待证等式的两边， 从上到下或从下到上读都会让我们到达上面化简等式的地方。剩下的等式单化简还不行， 我们还需要为推理链使用一个附加的运算符 _≡⟨_⟩_， 并将等式的依据放在尖括号中。这里给出的依据是：

⟨ cong suc (+-assoc m n p) ⟩

在这里，递归调用的 +-assoc m n p 拥有归纳假设的类型，而 cong suc 会在等式两边的前面加上 suc 以得到需要的等式。

若某个关系在应用了给定的函数后仍然保持不变，则称该关系满足合同性（Congruence）。 若 e 是 x ≡ y 的证据，那么对于任意函数 f，cong f e 就是 f x ≡ f y 的证据。

在这里并未假定归纳假设，而是通过递归调用我们定义的函数 +-assoc m n p 来证明。 对于加法，这是良基的（well-founded），因为更大数值的结合律可基于更小数值的结合律 来证明。在此步骤中，assoc (suc m) n p 是用 assoc m n p 证明的。 归纳证明和递归定义之间的这种对应是 Agda 中最吸引人的方面之一。

归纳即递归

下面是归纳如何对应于递归的具体例子，它是在结合律的证明中，将 m 实例化为 2 时的计算过程。

+-assoc-0 : ∀ (n p : ℕ) → ( + n) + p ≡  + (n + p)
+-assoc-0 n p =
  begin
    ( + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
     + (n + p)
  ∎

+-assoc-1 : ∀ (n p : ℕ) → ( + n) + p ≡  + (n + p)
+-assoc-1 n p =
  begin
    ( + n) + p
  ≡⟨⟩
    suc ( + n) + p
  ≡⟨⟩
    suc (( + n) + p)
  ≡⟨ cong suc (+-assoc-0 n p) ⟩
    suc ( + (n + p))
  ≡⟨⟩
     + (n + p)
  ∎

+-assoc-2 : ∀ (n p : ℕ) → ( + n) + p ≡  + (n + p)
+-assoc-2 n p =
  begin
    ( + n) + p
  ≡⟨⟩
    suc ( + n) + p
  ≡⟨⟩
    suc (( + n) + p)
  ≡⟨ cong suc (+-assoc-1 n p) ⟩
    suc ( + (n + p))
  ≡⟨⟩
     + (n + p)
  ∎

术语与记法

在结合律的陈述中出现的符号 ∀ 表示它对于所有的 m、n 和 p 都成立。 我们将 ∀ 称为全称量词（Universal Quantifier），我们会在 Quantifiers 章节中进一步讨论。

全称量词的证据是一个函数。函数签名

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

和

+-assoc : ∀ (m : ℕ) → ∀ (n : ℕ) → ∀ (p : ℕ) → (m + n) + p ≡ m + (n + p)

是等价的。和 ℕ → ℕ → ℕ 这样的函数类型不同，上述函数中的变量 与每一个实参类型相关联，且其结果类型可能会涉及（或依赖于）这些变量， 因此它们叫做依赖函数（Dependent Function）。

Ordinary functions are a special case of dependent functions. For instance, the signatures

_+_ : ℕ → ℕ → ℕ

and

_+_ : ∀ (m n : ℕ) → ℕ

and

_+_ : ∀ (m : ℕ) → ∀ (n : ℕ) → ℕ

are all equivalent.

第二个证明：交换律

加法的另一个重要性质是满足交换律（Commutativity），即运算数的顺序无关紧要：

m + n ≡ n + m

要证明它，我们需要先证明两条引理（Lemma）。

第一条引理

加法定义的起始步骤说明零是一个左幺元：

zero + n ≡ n

我们的第一条引理则说明零也是一个右幺元：

m + zero ≡ m

下面是该引理的陈述和证明：

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identityʳ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityʳ m) ⟩
    suc m
  ∎

其签名说明我们定义的标识符 +-identityʳ 提供了以下命题的证据：

∀ (m : ℕ) → m + zero ≡ m

该命题的证据是一个函数，它接受一个自然数，将其绑定到 m，然后返回 该等式对应实例的证据。它通过对 m 进行归纳来证明。

对于起始步骤，我们必须证明：

zero + zero ≡ zero

根据加法的起始步骤化简，这很显然。

对于归纳步骤，我们必须证明：

(suc m) + zero = suc m

根据加法的归纳步骤化简等式两边可得：

suc (m + zero) = suc m

反之，它也可以通过在归纳假设

m + zero ≡ m

两边之前加上 suc 得到。

阅读此等式链，从上到下和从下到上读都会让我们到达上面化简等式的地方。 剩下的等式可由以下依据得出：

⟨ cong suc (+-identityʳ m) ⟩

在这里，递归调用的 +-identityʳ m 拥有归纳假设的类型，而 cong suc 会在等式两边的前面加上 suc 以得到需要的等式。第一条引理证毕。

第二条引理

加法定义的归纳步骤将第一个参数的 suc 推到了外面：

suc m + n ≡ suc (m + n)

我们的第二条引理则对第二个参数的 suc 做同样的事情：

m + suc n ≡ suc (m + n)

下面是该引理的陈述和证明：

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

其签名说明我们定义的标识符 +-suc 提供了以下命题的证据：

∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

该命题的证据是一个函数，它接受两个自然数，将二者分别绑定到 m 和 n， 并返回该等式对应实例的证据。它通过对 m 进行归纳来证明。

对于起始步骤，我们必须证明：

zero + suc n ≡ suc (zero + n)

根据加法的起始步骤化简，这很显然。

对于归纳步骤，我们必须证明：

suc m + suc n ≡ suc (suc m + n)

根据加法的归纳步骤化简等式两边可得：

suc (m + suc n) ≡ suc (suc (m + n))

反之，它也可以通过在归纳假设

m + suc n ≡ suc (m + n)

两边之前加上 suc 得到。

从上到下或从下到上阅读等式链都会让我们在中间遇到化简后的等式。剩下的等式 可由以下依据得出：

⟨ cong suc (+-suc m n) ⟩

在这里，递归调用的 +-suc m n 拥有归纳假设的类型，而 cong suc 会在等式两边的前面加上 suc 以得到需要的等式。第二条引理证毕。

命题

最后，以下是我们的命题的陈述和证明：

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

第一行说明我们定义的标识符 +-comm 提供了以下命题的证据：

∀ (m n : ℕ) → m + n ≡ n + m

该命题的证据是一个函数，它接受两个自然数，将二者分别绑定到 m 和 n， 并返回该等式对应实例的证据。它通过对 n 进行归纳来证明。（这次不是 m！）

对于起始步骤，我们必须证明：

m + zero ≡ zero + m

根据加法的起始步骤化简等式两边可得：

m + zero ≡ m

剩下的等式可由依据 ⟨ +-identityʳ m ⟩ 得出，它调用第一条引理。

对于归纳步骤，我们必须证明：

m + suc n ≡ suc n + m

根据加法的归纳步骤化简等式两边可得：

m + suc n ≡ suc (n + m)

我们分两步来证明它。首先，我们有：

m + suc n ≡ suc (m + n)

它依据第二条引理 ⟨ +-suc m n ⟩ 得出。之后我们有：

suc (m + n) ≡ suc (n + m)

它依据合同性和归纳假设 ⟨ cong suc (+-comm m n) ⟩ 得出。证毕。

Agda 要求标识符必须在使用前定义，因此我们必须在主命题之前列出引理， 如前例所示。在实践中，我们通常会先试着证明主命题，之后所需的等式会说明 需要证明哪些引理。

第一个推论：重排定理

我们可以随意应用结合律来重排括号。例如：

+-rearrange : ∀ (m n p q : ℕ) → (m + n) + (p + q) ≡ m + (n + p) + q
+-rearrange m n p q =
  begin
    (m + n) + (p + q)
  ≡⟨ sym (+-assoc (m + n) p q) ⟩
    ((m + n) + p) + q
  ≡⟨ cong (_+ q) (+-assoc m n p) ⟩
    (m + (n + p)) + q
  ∎

无需归纳法，我们只不过应用了两次结合律就完成了证明。其中有几点需要注意的地方。

第一，加法是左结合的，因此 m + (n + p) + q 表示 (m + (n + p)) + q。

第二，我们用 sym 来交换等式的两边。命题 +-assoc (m + n) p q 会将括号从左边移到右边：

((m + n) + p) + q ≡ (m + n) + (p + q)

要往另一个方向移动括号，我们要用 sym (+-assoc (m + n) p q)：

(m + n) + (p + q) ≡ ((m + n) + p) + q

一般来说，若 e 提供了 x ≡ y 的证据，那么 sym e 就提供了 y ≡ x 的证据。

第三，Agda 支持 Richard Bird 引入的片段（Section）记法。我们将应用到 x 并返回 x + y 的函数写作 (_+ y)。因此，对于 assoc m n p 应用合同性 cong (_+ q) 会将等式：

(m + n) + p  ≡  m + (n + p)

转换成:

((m + n) + p) + q  ≡  (m + (n + p)) + q

类似地，我们将应用到 x 并返回 x + y 的函数写作 (x +_ )。 这同样适用于任何中缀运算符。

创世，最后一次

我们回到结合律的证明上来，把归纳证明（或等价的递归定义）看做一个创世故事会有助于理解。 这次我们专注于判断结合律的断言：

 -- 起初，我们对结合律一无所知。

现在，我们将规则应用到所有已知的判断上来。起始步骤告诉我们对于所有的自然数 n 和 p 来说，(zero + n) + p ≡ zero + (n + p)。归纳步骤告我我们若 (m + n) + p ≡ m + (n + p)（在昨天）成立，那么 (suc m + n) + p ≡ suc m + (n + p) （在今天）也成立。我们在今天之前并不知道任何关于结合律的判断， 因此此规则并未给出任何新的判断：

-- 第一天，我们知道了关于 0 的结合律。
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...

之后我们重复此过程，因此接下来一天我们知道今天以前的所有判断， 以及任何通过此规则添加的判断。起始步骤并未告诉我们新的东西， 而如今归归纳步骤添加了更多的判断：

-- 第二天，我们知道了关于 0 和 1 的结合律。
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...

我们再次重复此过程：

-- 第三天，我们知道了关于 0、1 和 2 的结合律。
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...
(2 + 0) + 0 ≡ 2 + (0 + 0)   ...   (2 + 4) + 5 ≡ 2 + (4 + 5)   ...

此时规律已经很明显了：

-- 第四天，我们知道了关于 0、1、2 和 3 的结合律。
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...
(2 + 0) + 0 ≡ 2 + (0 + 0)   ...   (2 + 4) + 5 ≡ 2 + (4 + 5)   ...
(3 + 0) + 0 ≡ 3 + (0 + 0)   ...   (3 + 4) + 5 ≡ 3 + (4 + 5)   ...

此过程可以继续下去。在第 m 天我们会知道所有第一个数小于 m 的判断。

还有一种完全有限的方法来生成同样的等式，它的证明留作读者的练习。

练习 finite-+-assoc（延伸）

请参考前文写出前四天已知的加法结合律的创世故事。

-- 请将代码写在此处。

用改写来证明结合律

证明可不止一种方法。下面是第二种在 Agda 中证明加法结合律的方法，使用 rewrite（改写） 而非等式链：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero    n p                          =  refl
+-assoc′ (suc m) n p  rewrite +-assoc′ m n p  =  refl

对于起始步骤，我们必须证明：

(zero + n) + p ≡ zero + (n + p)

根据加法的起始步骤化简等式两边可得：

n + p ≡ n + p

此式平凡成立。一个项等于其自身的证明写作 refl（自反性）。

对于归纳步骤，我们必须证明：

(suc m + n) + p ≡ suc m + (n + p)

根据加法的归纳步骤化简等式两边可得：

suc ((m + n) + p) ≡ suc (m + (n + p))

This is our goal to be proved. Rewriting by a given equation is indicated by the keyword rewrite followed by a proof of that equation. Rewriting replaces each occurrence of the left-hand side of the equation in the goal by the right-hand side. In this case, after rewriting by the inductive hypothesis our goal becomes

suc (m + (n + p)) ≡ suc (m + (n + p))

其证明同样由 refl 给出。改写不仅可以省去等式链还可以避免调用 cong.

使用改写证明交换律

下面是加法交换律的第二个证明，使用 rewrite 而非等式链：

+-identity′ : ∀ (n : ℕ) → n + zero ≡ n
+-identity′ zero = refl
+-identity′ (suc n) rewrite +-identity′ n = refl

+-suc′ : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc′ zero n = refl
+-suc′ (suc m) n rewrite +-suc′ m n = refl

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ m zero rewrite +-identity′ m = refl
+-comm′ m (suc n) rewrite +-suc′ m n | +-comm′ m n = refl

在最后一行中，用两个等式进行改写被表示为用一条竖线分隔两个相关等式的证明。 左边的改写会在右边之前被执行。

交互式构造证明

看看如何在 Emacs 中用 Agda 的交互式特性来构造另一种结合律的证明会很有启发性。 我们从输入以下内容开始：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ m n p = ?

其中的问号表示你想要 Agda 帮你填充的代码。如果你按下 C-c C-l （先按 Ctrl-c 再按 Ctrl-l），那么问号会被替换为：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ m n p = { }0

空的大括号叫做洞（Hole），0 是用来指代此洞的编号。洞可能会以绿色高亮显示。 Emacs 还会在屏幕下方创建一个新的窗口并显示文本：

?0 : ((m + n) + p) ≡ (m + (n + p))

这表示 0 号洞需要以所提示的判断的证明来填充。

我们希望对 m 进行归纳来证明此命题。将光标移动到洞中并按下 C-c C-c。它会给出提示：

pattern variables to case (empty for split on result):

按下 m 会拆分该变量，并更新此代码：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = { }0
+-assoc′ (suc m) n p = { }1

现在有两个洞了，下方的窗口会告诉你每个洞中需要证明的内容：

?0 : ((zero + n) + p) ≡ (zero + (n + p))
?1 : ((suc m + n) + p) ≡ (suc m + (n + p))

进入 0 号洞并按下 C-c C-, 会显示以下文本：

Goal: (n + p) ≡ (n + p)
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ

它表示在化简之后，0 号洞的目标如上所示，所示类型的变量 p 和 n 可在证明中使用。 给定目标的证明很平凡，只需进入该目标并按下 C-c C-r 即可填充。按下 C-c C-l 会将剩下的洞重新编号为 0：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p = { }0

进入新的 0 号洞并按下 C-c C-, 会显示以下文本：

Goal: suc ((m + n) + p) ≡ suc (m + (n + p))
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ
m : ℕ

同样，它会给出化简后的目标和可用的变量。在此步骤中，我们需要根据归纳假设进行改写， 于是我们来编辑这些文本：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = { }0

进入剩下的洞中并按下 C-c C-, 会显示以下文本：

Goal: suc (m + (n + p)) ≡ suc (m + (n + p))
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ
m : ℕ

给定目标的证明很平凡，只需进入该目标并按下 C-c C-r 即可填充并完成证明：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl

练习：+-swap（推荐）

请证明对于所有的自然数 m、n 和 p，

m + (n + p) ≡ n + (m + p)

成立。无需归纳证明，只需应用前面满足结合律和交换律的结果即可。

-- 请将代码写在此处。

练习 *-distrib-+（推荐）

请证明乘法对加法满足分配律，即对于所有的自然数 m、n 和 p，

(m + n) * p ≡ m * p + n * p

成立。

-- 请将代码写在此处。

练习 *-assoc（推荐）

请证明乘法满足结合律，即对于所有的自然数 m、n 和 p，

(m * n) * p ≡ m * (n * p)

成立。

-- 请将代码写在此处。

练习 *-comm（实践）

请证明乘法满足交换律，即对于所有的自然数 m 和 n，

m * n ≡ n * m

成立。和加法交换律一样，你需要陈述并证明配套的引理。

-- 请将代码写在此处。

练习 0∸n≡0（实践）

请证明对于所有的自然数 n，

zero ∸ n ≡ zero

成立。你的证明需要归纳法吗？

-- 请将代码写在此处。

练习 ∸-+-assoc（实践）

请证明饱和减法与加法满足结合律，即对于所有的自然数 m、n 和 p，

m ∸ n ∸ p ≡ m ∸ (n + p)

成立。

-- 请将代码写在此处。

练习 +*^ （延伸）

证明下列三条定律

 m ^ (n + p) ≡ (m ^ n) * (m ^ p)  (^-distribˡ-+-*)
 (m * n) ^ p ≡ (m ^ p) * (n ^ p)  (^-distribʳ-*)
 (m ^ n) ^ p ≡ m ^ (n * p)        (^-*-assoc)

对于所有 m、n 和 p 成立。

-- 请将代码写在此处。

练习 Bin-laws（延伸）

回想练习 Bin 中定义的一种表示自然数的比特串数据类型 Bin 以及要求你定义的函数：

inc   : Bin → Bin
to    : ℕ → Bin
from  : Bin → ℕ

考虑以下定律，其中 n 表示自然数，b 表示比特串：

from (inc b) ≡ suc (from b)
to (from b) ≡ b
from (to n) ≡ n

对于每一条定律：若它成立，请证明；若不成立，请给出一个反例。

-- 请将代码写在此处。

标准库

本章中类似的定义可在标准库中找到：

import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)

Unicode

本章中使用了以下 Unicode：

∀  U+2200  对于所有 (\forall, \all)
ʳ  U+02B3  修饰符小写字母 r (\^r)
′  U+2032  撇号 (\')
″  U+2033  双撇号 (\')
‴  U+2034  三撇号 (\')
⁗  U+2057  四撇号 (\')

与 \r 类似，命令 \^r 列出了多种上标右箭头的变体，以及上标的字母 r。 命令 \' 列出了一些撇号（′ ″ ‴ ⁗）。

Relations: 关系的归纳定义

module plfa.part1.Relations where

在定义了加法和乘法等运算以后，下一步我们来定义关系（Relation），比如说小于等于。

导入

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm; +-identityʳ)

定义关系

小于等于这个关系有无穷个实例，如下所示：

0 ≤ 0     0 ≤ 1     0 ≤ 2     0 ≤ 3     ...
          1 ≤ 1     1 ≤ 2     1 ≤ 3     ...
                    2 ≤ 2     2 ≤ 3     ...
                              3 ≤ 3     ...
                                        ...

但是，我们仍然可以用几行有限的定义来表示所有的实例，如下文所示的一对推理规则：

z≤n --------
    zero ≤ n

    m ≤ n
s≤s -------------
    suc m ≤ suc n

以及其 Agda 定义：

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      --------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

在这里，z≤n 和 s≤s（无空格）是构造子的名称，zero ≤ n、m ≤ n 和 suc m ≤ suc n （带空格）是类型。在这里我们第一次用到了 索引数据类型（Indexed datatype）。我们使用 m 和 n 这两个自然数来索引 m ≤ n 这个类型。在 Agda 里，由两个及以上短横线开始的行是注释行， 我们巧妙利用这一语法特性，用上述形式来表示相应的推理规则。 在后文中，我们还会继续使用这一形式。

这两条定义告诉我们相同的两件事：

• 起始步骤: 对于所有的自然数 n，命题 zero ≤ n 成立。
• 归纳步骤：对于所有的自然数 m 和 n，如果命题 m ≤ n 成立， 那么命题 suc m ≤ suc n 成立。

实际上，他们分别给我们更多的信息：

• 起始步骤: 对于所有的自然数 n，构造子 z≤n 提供了 zero ≤ n 成立的证明。
• 归纳步骤：对于所有的自然数 m 和 n，构造子 s≤s 将 m ≤ n 成立的证明 转化为 suc m ≤ suc n 成立的证明。

例如，我们在这里以推理规则的形式写出 2 ≤ 4 的证明：

  z≤n -----
      0 ≤ 2
 s≤s -------
      1 ≤ 3
s≤s ---------
      2 ≤ 4

下面是对应的 Agda 证明：

_ :  ≤ 
_ = s≤s (s≤s z≤n)

隐式参数

这是我们第一次使用隐式参数。定义不等式时，构造子的定义中使用了 ∀， 就像我们在下面的命题中使用 ∀ 一样：

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m

但是我们这里的定义使用了花括号 { }，而不是小括号 ( )。 这意味着参数是隐式的（Implicit），不需要额外声明。实际上，Agda 的类型检查器 会推导（Infer）出它们。因此，我们在 m + n ≡ n + m 的证明中需要写出 +-comm m n， 在 zero ≤ n 的证明中可以省略 n。同理，如果 m≤n 是 m ≤ n的证明， 那么我们写出 s≤s m≤n 作为 suc m ≤ suc n 的证明，无需声明 m 和 n。

如果有希望的话，我们也可以在大括号里显式声明隐式参数。例如，下面是 2 ≤ 4 的 Agda 证明，包括了显式声明了的隐式参数：

_ :  ≤ 
_ = s≤s {} {} (s≤s {} {} (z≤n {}))

也可以额外加上参数的名字：

_ :  ≤ 
_ = s≤s {m = } {n = } (s≤s {m = } {n = } (z≤n {n = }))

在后者的形式中，也可以选择只声明一部分隐式参数：

_ :  ≤ 
_ = s≤s {n = } (s≤s {n = } z≤n)

但是不可以改变隐式参数的顺序，即便加上了名字。

我们可以写出 _ 来让 Agda 用相同的推导方式试着推导一个显式的项。 例如，我们可以为命题 +-identityʳ 定义一个带有隐式参数的变体：

+-identityʳ′ : ∀ {m : ℕ} → m + zero ≡ m
+-identityʳ′ = +-identityʳ _

我们用 _ 来让 Agda 从语境中推导显式参数的值。只有 m 这一个值能够给出正确的证明，因此 Agda 愉快地填入了它。 如果 Agda 推导值失败，那么它会报一个错误。

优先级

我们如下定义比较的优先级：

infix  _≤_

我们将 _≤_ 的优先级设置为 4，所以它不如优先级为 6 的 _+_ 结合得紧，因而， 1 + 2 ≤ 3 将被解析为 (1 + 2) ≤ 3。我们用 infix 来表示运算符既不是左结合的， 也不是右结合的。因为 1 ≤ 2 ≤ 3 解析为 (1 ≤ 2) ≤ 3 或者 1 ≤ (2 ≤ 3) 都没有意义。

可判定性

给定两个数，我们可以很直接地决定第一个数是不是小于等于第二个数。我们在此处不给出说明的代码， 但我们会在 Decidable 章节重新讨论这个问题。

反演

在我们的定义中，我们从更小的东西得到更大的东西。例如，我们可以从 m ≤ n 得出 suc m ≤ suc n 的结论，这里的 suc m 比 m 更大 （也就是说，前者包含后者），suc n 也比 n 更大。但有时我们也 需要从更大的东西得到更小的东西。

只有一种方式能够证明对于任意 m 和 n 有 suc m ≤ suc n。 这让我们能够反演（invert）之前的规则。

inv-s≤s : ∀ {m n : ℕ}
  → suc m ≤ suc n
    -------------
  → m ≤ n
inv-s≤s (s≤s m≤n) = m≤n

这里的 m≤n（不带空格）是一个变量名，而 m ≤ n（带空格）是一个类型， 且后者是前者的类型。在 Agda 中，将类型中的空格去掉来作为变量名是一种常见的约定。

并不是所有规则都可以反演。实际上，z≤n 的规则没有非隐式的假设， 因此它没有可以被反演的规则。但这种反演通常是成立的。

反演的另一个例子是证明只存在一种情况使得一个数字能够小于或等于零。

inv-z≤n : ∀ {m : ℕ}
  → m ≤ zero
    --------
  → m ≡ zero
inv-z≤n z≤n = refl

序关系的性质

数学家对于关系的常见性质给出了约定的名称。

• 自反（Reflexive）：对于所有的 n，关系 n ≤ n 成立。
• 传递（Transitive）：对于所有的 m、 n 和 p，如果 m ≤ n 和 n ≤ p 成立，那么 m ≤ p 也成立。
• 反对称（Anti-symmetric）：对于所有的 m 和 n，如果 m ≤ n 和 n ≤ m 同时成立，那么 m ≡ n 成立。
• 完全（Total）：对于所有的 m 和 n，m ≤ n 或者 n ≤ m 成立。

_≤_ 关系满足上述四条性质。

对于上述性质的组合也有约定的名称。

• 预序（Preorder）：满足自反和传递的关系。
• 偏序（Partial Order）：满足反对称的预序。
• 全序（Total Order）：满足完全的偏序。

如果你在派对上偶遇一个『关系』，你现在知道怎么样和人讨论了， 可以讨论关于自反、传递、反对称和完全， 或者问一问这是不是预序、偏序或者全序。

更认真的来说，如果你在阅读论文时碰到了一个关系，本文的介绍让你可以对关系有基本的了解和判断， 来判断这个关系是不是预序、偏序或者全序。一个认真的作者一般会在文章指出这个关系具有（或者缺少） 上述性质，比如说指出新定义的关系是一个偏序而不是全序。

练习 orderings（实践）

给出一个不是偏序的预序的例子。

-- 请将代码写在此处。

给出一个不是全序的偏序的例子。

-- 请将代码写在此处。

自反性

我们第一个来证明的性质是自反性：对于任意自然数 n，关系 n ≤ n 成立。我们使用标准库 的惯例来隐式申明参数，在使用自反性的证明时这样可以更加方便。

≤-refl : ∀ {n : ℕ}
    -----
  → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl

这个证明直接在 n 上进行归纳。在起始步骤中，zero ≤ zero 由 z≤n 证明；在归纳步骤中， 归纳假设 ≤-refl {n} 给我们带来了 n ≤ n 的证明，我们只需要使用 s≤s，就可以获得 suc n ≤ suc n 的证明。

在 Emacs 中来交互式地证明自反性是一个很好的练习，可以使用洞，以及 C-c C-c、 C-c C-, 和 C-c C-r 命令。

传递性

我们第二个证明的性质是传递性：对于任意自然数 m 和 n，如果 m ≤ n 和 n ≤ p 成立，那么 m ≤ p 成立。同样，m、n 和 p 是隐式参数：

≤-trans : ∀ {m n p : ℕ}
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans z≤n       _          =  z≤n
≤-trans (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans m≤n n≤p)

这里我们在 m ≤ n 的证据（Evidence）上进行归纳。在起始步骤里，第一个不等式因为 z≤n 而成立， 那么结论亦可由 z≤n 而得出。在这里，n ≤ p 的证明是不需要的，我们用 _ 来表示这个 证明没有被使用。

在归纳步骤中，第一个不等式因为 s≤s m≤n 而成立，第二个不等式因为 s≤s n≤p 而成立， 所以我们已知 suc m ≤ suc n 和 suc n ≤ suc p，求证 suc m ≤ suc p。 通过归纳假设 ≤-trans m≤n n≤p，我们得知 m ≤ p，在此之上使用 s≤s 即可证。

≤-trans (s≤s m≤n) z≤n 不可能发生，因为第一个不等式告诉我们中间的数是一个 suc n， 而第二个不等式告诉我们中间的数是 zero。Agda 可以推断这样的情况不可能发现，所以我们不需要 （也不可以）列出这种情况。

我们也可以将隐式参数显式地声明。

≤-trans′ : ∀ (m n p : ℕ)
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans′ zero    _       _       z≤n       _          =  z≤n
≤-trans′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans′ m n p m≤n n≤p)

有人说这样的证明更加的清晰，也有人说这个更长的证明让人难以抓住证明的重点。 我们一般选择使用简短的证明。

对于性质成立证明进行的归纳（如上文中对于 m ≤ n 的证明进行归纳），相比于对于性质成立的值进行的归纳 （如对于 m 进行归纳），有非常大的价值。我们会经常使用这样的方法。

同样，在 Emacs 中来交互式地证明传递性是一个很好的练习，可以使用洞，以及 C-c C-c、 C-c C-, 和 C-c C-r 命令。

反对称性

我们证明的第三个性质是反对称性：对于所有的自然数 m 和 n，如果 m ≤ n 和 n ≤ m 同时成立，那么 m ≡ n 成立：

≤-antisym : ∀ {m n : ℕ}
  → m ≤ n
  → n ≤ m
    -----
  → m ≡ n
≤-antisym z≤n       z≤n        =  refl
≤-antisym (s≤s m≤n) (s≤s n≤m)  =  cong suc (≤-antisym m≤n n≤m)

同样，我们对于 m ≤ n 和 n ≤ m 的证明进行归纳。

在起始步骤中，两个不等式都因为 z≤n 而成立。因此我们已知 zero ≤ zero 和 zero ≤ zero， 求证 zero ≡ zero，由自反性可证。（注：由等式的自反性可证，而不是不等式的自反性）

在归纳步骤中，第一个不等式因为 s≤s m≤n 而成立，第二个等式因为 s≤s n≤m 而成立。因此我们已知 suc m ≤ suc n 和 suc n ≤ suc m，求证 suc m ≡ suc n。归纳假设 ≤-antisym m≤n n≤m 可以证明 m ≡ n，因此我们可以使用同余性完成证明。

练习 ≤-antisym-cases（实践）

上面的证明中省略了一个参数是 z≤n，另一个参数是 s≤s 的情况。为什么可以省略这种情况？

-- 请将代码写在此处。

完全性

我们证明的第四个性质是完全性：对于任何自然数 m 和 n，m ≤ n 或者 n ≤ m 成立。 在 m 和 n 相等时，两者同时成立。

我们首先来说明怎么样不等式才是完全的：

data Total (m n : ℕ) : Set where

  forward :
      m ≤ n
      ---------
    → Total m n

  flipped :
      n ≤ m
      ---------
    → Total m n

Total m n 成立的证明有两种形式：forward m≤n 或者 flipped n≤m，其中 m≤n 和 n≤m 分别是 m ≤ n 和 n ≤ m 的证明。

（如果你对于逻辑学有所了解，上面的定义可以由析取（Disjunction）表示。 我们会在 Connectives 章节介绍析取。）

这是我们第一次使用带参数的数据类型，这里 m 和 n 是参数。这等同于下面的索引数据类型：

data Total′ : ℕ → ℕ → Set where

  forward′ : ∀ {m n : ℕ}
    → m ≤ n
      ----------
    → Total′ m n

  flipped′ : ∀ {m n : ℕ}
    → n ≤ m
      ----------
    → Total′ m n

类型里的每个参数都转换成构造子的一个隐式参数。索引数据类型中的索引可以变化，正如在 zero ≤ n 和 suc m ≤ suc n 中那样，而参数化数据类型不一样，其参数必须保持相同， 正如在 Total m n 中那样。参数化的声明更短，更易于阅读，而且有时可以帮助到 Agda 的 停机检查器，所以我们尽可能地使用它们，而不是索引数据类型。

在上述准备工作完成后，我们定义并证明完全性。

≤-total : ∀ (m n : ℕ) → Total m n
≤-total zero    n                         =  forward z≤n
≤-total (suc m) zero                      =  flipped z≤n
≤-total (suc m) (suc n) with ≤-total m n
...                        | forward m≤n  =  forward (s≤s m≤n)
...                        | flipped n≤m  =  flipped (s≤s n≤m)

这里，我们的证明在两个参数上进行归纳，并按照情况分析：

• 第一起始步骤：如果第一个参数是 zero，第二个参数是 n，那么 forward 条件成立，我们使用 z≤n 作为 zero ≤ n 的证明。

• 第二起始步骤：如果第一个参数是 suc m，第二个参数是 zero，那么 flipped 条件成立，我们使用 z≤n 作为 zero ≤ suc m 的证明。

• 归纳步骤：如果第一个参数是 suc m，第二个参数是 suc n，那么归纳假设 ≤-total m n 可以给出如下推断：

  • 归纳假设的 forward 条件成立，以 m≤n 作为 m ≤ n 的证明。以此我们可以使用 s≤s m≤n 作为 suc m ≤ suc n 来证明 forward 条件成立。

  • 归纳假设的 flipped 条件成立，以 n≤m 作为 n ≤ m 的证明。以此我们可以使用 s≤s n≤m 作为 suc n ≤ suc m 来证明 flipped 条件成立。

这是我们第一次在 Agda 中使用 with 语句。with 关键字后面有一个表达式和一或多行。 每行以省略号（...）和一个竖线（|）开头，后面跟着用来匹配表达式的模式，和等式的右手边。

使用 with 语句等同于定义一个辅助函数。比如说，上面的定义和下面的等价：

≤-total′ : ∀ (m n : ℕ) → Total m n
≤-total′ zero    n        =  forward z≤n
≤-total′ (suc m) zero     =  flipped z≤n
≤-total′ (suc m) (suc n)  =  helper (≤-total′ m n)
  where
  helper : Total m n → Total (suc m) (suc n)
  helper (forward m≤n)  =  forward (s≤s m≤n)
  helper (flipped n≤m)  =  flipped (s≤s n≤m)

这也是我们第一次在 Agda 中使用 where 语句。where 关键字后面有一或多条定义，其必须被缩进。 之前等式左手边的约束变量（此例中的 m 和 n）在嵌套的定义中仍然在作用域内。 在嵌套定义中的约束标识符（此例中的 helper ）在等式的右手边的作用域内。

如果两个参数相同，那么两个情况同时成立，我们可以返回任一证明。上面的代码中我们返回 forward 条件， 但是我们也可以返回 flipped 条件，如下：

≤-total″ : ∀ (m n : ℕ) → Total m n
≤-total″ m       zero                      =  flipped z≤n
≤-total″ zero    (suc n)                   =  forward z≤n
≤-total″ (suc m) (suc n) with ≤-total″ m n
...                         | forward m≤n  =  forward (s≤s m≤n)
...                         | flipped n≤m  =  flipped (s≤s n≤m)

两者的区别在于上述代码在对于第一个参数进行模式匹配之前先对于第二个参数先进行模式匹配。

单调性

如果在聚会中碰到了一个运算符和一个序，那么有人可能会问这个运算符对于这个序是不是 单调的（Monotonic）。比如说，加法对于小于等于是单调的，这意味着：

∀ {m n p q : ℕ} → m ≤ n → p ≤ q → m + p ≤ n + q

这个证明可以用我们学会的方法，很直接的来完成。我们最好把它分成三个部分，首先我们证明加法对于 小于等于在右手边是单调的：

+-monoʳ-≤ : ∀ (n p q : ℕ)
  → p ≤ q
    -------------
  → n + p ≤ n + q
+-monoʳ-≤ zero    p q p≤q  =  p≤q
+-monoʳ-≤ (suc n) p q p≤q  =  s≤s (+-monoʳ-≤ n p q p≤q)

我们对于第一个参数进行归纳。

• 起始步骤：第一个参数是 zero，那么 zero + p ≤ zero + q 可以化简为 p ≤ q， 其证明由 p≤q 给出。

• 归纳步骤：第一个参数是 suc n，那么 suc n + p ≤ suc n + q 可以化简为 suc (n + p) ≤ suc (n + q)。归纳假设 +-monoʳ-≤ n p q p≤q 可以证明 n + p ≤ n + q，我们在此之上使用 s≤s 即可得证。

接下来，我们证明加法对于小于等于在左手边是单调的。我们可以用之前的结论和加法的交换律来证明：

+-monoˡ-≤ : ∀ (m n p : ℕ)
  → m ≤ n
    -------------
  → m + p ≤ n + p
+-monoˡ-≤ m n p m≤n  rewrite +-comm m p | +-comm n p  = +-monoʳ-≤ p m n m≤n

用 +-comm m p 和 +-comm n p 来重写，可以让 m + p ≤ n + p 转换成 p + n ≤ p + m， 而我们可以用 +-moroʳ-≤ p m n m≤n 来证明。

最后，我们把前两步的结论结合起来：

+-mono-≤ : ∀ (m n p q : ℕ)
  → m ≤ n
  → p ≤ q
    -------------
  → m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q  =  ≤-trans (+-monoˡ-≤ m n p m≤n) (+-monoʳ-≤ n p q p≤q)

使用 +-monoˡ-≤ m n p m≤n 可以证明 m + p ≤ n + p， 使用 +-monoʳ-≤ n p q p≤q 可以证明 n + p ≤ n + q，用传递性把两者连接起来， 我们可以获得 m + p ≤ n + q 的证明，如上所示。

练习 *-mono-≤ （延伸）

证明乘法对于小于等于是单调的。

-- 请将代码写在此处。

严格不等关系

我们可以用类似于定义不等关系的方法来定义严格不等关系。

infix  _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

  s<s : ∀ {m n : ℕ}
    → m < n
      -------------
    → suc m < suc n

严格不等关系与不等关系最重要的区别在于，0 小于任何数的后继，而不小于 0。

显然，严格不等关系不是自反的，而是非自反的（Irreflexive），表示 n < n 对于 任何值 n 都不成立。和不等关系一样，严格不等关系是传递的。严格不等关系不是完全的，但是满足 一个相似的性质：三分律（Trichotomy）：对于任意的 m 和 n，m < n、m ≡ n 或者 m > n 三者有且仅有一者成立。（我们定义 m > n 当且仅当 n < m 成立时成立） 严格不等关系对于加法和乘法也是单调的。

我们把一部分上述性质作为习题。非自反性需要逻辑非，三分律需要证明三者是互斥的，因此这两个性质 暂不做为习题。我们会在 Negation 章节来重新讨论。

我们可以直接地来证明 suc m ≤ n 蕴涵了 m < n，及其逆命题。 因此我们亦可从不等关系的性质中，使用此性质来证明严格不等关系的性质。

练习 <-trans （推荐）

证明严格不等是传递的。请直接证明。（后续的练习中我们将使用 < 和 ≤ 的关系。）

-- 请将代码写在此处。

练习 trichotomy（实践）

证明严格不等关系满足弱化的三元律，证明对于任意 m 和 n，下列命题有一条成立：

• m < n，
• m ≡ n，或者
• m > n。

定义 m > n 为 n < m。你需要一个合适的数据类型声明，如同我们在证明完全性中使用的那样。 （我们会在介绍完否定之后证明三者是互斥的。）

-- 请将代码写在此处。

练习 +-mono-<（实践）

证明加法对于严格不等关系是单调的。正如不等关系中那样，你可以需要额外的定义。

-- 请将代码写在此处。

练习 ≤-iff-< (推荐)

证明 suc m ≤ n 蕴涵了 m < n，及其逆命题。

-- 请将代码写在此处。

练习 <-trans-revisited（实践）

用另外一种方法证明严格不等是传递的，使用之前证明的不等关系和严格不等关系的联系， 以及不等关系的传递性。

-- 请将代码写在此处。

奇和偶

作为一个额外的例子，我们来定义奇数和偶数。不等关系和严格不等关系是二元关系，而奇偶性 是一元关系，有时也被叫做谓词（Predicate）：

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  zero :
      ---------
      even zero

  suc  : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where

  suc  : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

一个数是偶数，如果它是 0，或者是奇数的后继。一个数是奇数，如果它是偶数的后继。

这是我们第一次定义一个相互递归的数据类型。因为每个标识符必须在使用前声明，所以 我们首先声明索引数据类型 even 和 odd （省略 where 关键字和其构造子的定义）， 然后声明其构造子（省略其签名 ℕ → Set，因为在之前已经给出）。

这也是我们第一次使用重载（Overloaded）的构造子。这意味着不同类型的构造子 拥有相同的名字。在这里 suc 表示下面三种构造子其中之一：

suc : ℕ → ℕ

suc : ∀ {n : ℕ}
  → odd n
    ------------
  → even (suc n)

suc : ∀ {n : ℕ}
  → even n
    -----------
  → odd (suc n)

同理，zero 表示两种构造子的一种。因为类型推导的限制，Agda 不允许重载已定义的名字， 但是允许重载构造子。我们推荐将重载限制在有关联的定义中，如我们所做的这样，但这不是必须的。

我们证明两个偶数之和是偶数：

e+e≡e : ∀ {m n : ℕ}
  → even m
  → even n
    ------------
  → even (m + n)

o+e≡o : ∀ {m n : ℕ}
  → odd m
  → even n
    -----------
  → odd (m + n)

e+e≡e zero     en  =  en
e+e≡e (suc om) en  =  suc (o+e≡o om en)

o+e≡o (suc em) en  =  suc (e+e≡e em en)

与相互递归的定义对应，我们用两个相互递归的函数，一个证明两个偶数之和是偶数，另一个证明 一个奇数与一个偶数之和是奇数。

这是我们第一次使用相互递归的函数。因为每个标识符必须在使用前声明，我们先给出两个函数的签名， 然后再给出其定义。

要证明两个偶数之和为偶，我们考虑第一个数为偶数的证明。如果是因为第一个数为 0， 那么第二个数为偶数的证明即为和为偶数的证明。如果是因为第一个数为奇数的后继， 那么和为偶数是因为他是一个奇数和一个偶数的和的后续，而这个和是一个奇数。

要证明一个奇数和一个偶数的和是奇数，我们考虑第一个数是奇数的证明。 如果是因为它是一个偶数的后继，那么和为奇数，因为它是两个偶数之和的后继， 而这个和是一个偶数。

练习 o+o≡e (延伸)

证明两个奇数之和为偶数。

-- 请将代码写在此处。

练习 Bin-predicates (延伸)

回忆我们在练习 Bin 中定义了一个数据类型 Bin 来用二进制字符串表示自然数。 这个表达方法不是唯一的，因为我们在开头加任意个 0。因此，11 可以由以下方法表示：

⟨⟩ I O I I
⟨⟩ O O I O I I

定义一个谓词

Can : Bin → Set

其在一个二进制字符串的表示是标准的（Canonical）时成立，表示它没有开头的 0。在两个 11 的表达方式中， 第一个是标准的，而第二个不是。在定义这个谓词时，你需要一个辅助谓词：

One : Bin → Set

其仅在一个二进制字符串开头为 1 时成立。一个二进制字符串是标准的，如果它开头是 1 （表示一个正数）， 或者它仅是一个 0 （表示 0）。

证明递增可以保持标准性。

Can b
------------
Can (inc b)

证明从自然数转换成的二进制字符串是标准的。

----------
Can (to n)

证明将一个标准的二进制字符串转换成自然数之后，再转换回二进制字符串与原二进制字符串相同。

Can b
---------------
to (from b) ≡ b

提示：对于每一条习题，先从 One 的性质开始。 证明以下命题也会很有帮助。

One b
----------
1 ≤ from b

1 ≤ n
---------------------
to (2 * n) ≡ (to n) O

-- 请将代码写在此处。

标准库

标准库中有类似于本章介绍的定义：

import Data.Nat using (_≤_; z≤n; s≤s)
import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
                                  +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)

在标准库中，≤-total 是使用析取定义的（我们将在 Connectives 章节定义）。 +-monoʳ-≤、+-monoˡ-≤ 和 +-mono-≤ 的证明方法和本书不同。 更多的参数是隐式申明的。

Unicode

本章使用了如下 Unicode 符号：

≤  U+2264  小于等于 (\<=, \le)
≥  U+2265  大于等于 (\>=, \ge)
ˡ  U+02E1  小写字母 L 标识符 (\^l)
ʳ  U+02B3  小写字母 R 标识符 (\^r)

\^l 和 \^r 命令给出了左右箭头，以及上标字母 l 和 r。

Equality: 相等性与等式推理

module plfa.part1.Equality where

我们在论证的过程中经常会使用相等性。给定两个都为 A 类型的项 M 和 N， 我们用 M ≡ N 来表示 M 和 N 可以相互替换。在此之前， 我们将相等性作为一个基础运算，而现在我们来说明如何将其定义为一个归纳的数据类型。

导入

本章节没有导入的内容。本书的每一章节，以及 Agda 标准库的每个模块都导入了相等性。 我们在此定义相等性，导入其他内容将会产生冲突。

相等性

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

用其他的话来说，对于任意类型 A 和任意 A 类型的 x，构造子 refl 提供了 x ≡ x 的证明。所以，每个值等同于它本身，我们并没有其他办法来证明值的相等性。 这个定义里有不对称的地方，_≡_ 的第一个参数（Argument）由 x : A 给出， 而第二个参数（Argument）则是由 A → Set 的索引给出。 这和我们尽可能多的使用参数（Parameter）的理念相符。_≡_ 的第一个参数（Argument） 可以作为一个参数（Parameter），因为它不会变，而第二个参数（Argument）则必须是一个索引， 这样它才可以等于第一个。

我们如下定义相等性的优先级：

infix  _≡_

我们将 _≡_ 的优先级设置为 4，与 _≤_ 相同，所以其它算术运算符的结合都比它紧密。 由于它既不是左结合，也不是右结合的，因此 x ≡ y ≡ z 是不合法的。

相等性是一个等价关系（Equivalence Relation）

一个等价关系是自反、对称和传递的。其中自反性可以通过构造子 refl 直接从相等性的定义中得来。 我们可以直接地证明其对称性：

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = refl

这个证明是怎么运作的呢？sym 参数的类型是 x ≡ y，但是等式的左手边被 refl 模式实例化了， 这要求 x 和 y 相等。因此，等式的右手边需要一个类型为 x ≡ x 的项，用 refl 即可。

交互式地证明 sym 很有教育意义。首先，我们在左手边使用一个变量来表示参数，在右手边使用一个洞：

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym e = {! !}

如果我们进入这个洞，使用 C-c C-,，Agda 会告诉我们：

Goal: .y ≡ .x
————————————————————————————————————————————————————————————
e  : .x ≡ .y
.y : .A
.x : .A
.A : Set

在这个洞里，我们使用 C-c C-c e，Agda 会将 e 逐一展开为所有可能的构造子。 此处只有一个构造子：

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = {! !}

如果我们再次进入这个洞，重新使用 C-c C-,，然后 Agda 现在会告诉我们：

 Goal: .x ≡ .x
 ————————————————————————————————————————————————————————————
 .x : .A
 .A : Set

这是一个重要的步骤—— Agda 发现了 x 和 y 必须相等，才能与模式 refl 相匹配。

最后，我们回到洞里，使用 C-c C-r，Agda 将会把洞变成一个可以满足给定类型的构造子实例。

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = refl

我们至此完成了与之前给出证明相同的证明。

传递性亦是很直接：

trans : ∀ {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
    -----
  → x ≡ z
trans refl refl  =  refl

同样，交互式地证明这个特性是一个很好的练习，尤其是观察 Agda 的已知内容根据参数的实例而变化的过程。

合同性和替换性

相等性满足合同性（Congruence）。如果两个项相等，那么对它们使用相同的函数， 其结果仍然相等：

cong : ∀ {A B : Set} (f : A → B) {x y : A}
  → x ≡ y
    ---------
  → f x ≡ f y
cong f refl  =  refl

两个参数的函数也满足合同性：

cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B}
  → u ≡ x
  → v ≡ y
    -------------
  → f u v ≡ f x y
cong₂ f refl refl  =  refl

在函数上的等价性也满足合同性。如果两个函数是相等的，那么它们作用在同一项上的结果是相等的：

cong-app : ∀ {A B : Set} {f g : A → B}
  → f ≡ g
    ---------------------
  → ∀ (x : A) → f x ≡ g x
cong-app refl x = refl

相等性也满足替换性（Substitution）。 如果两个值相等，其中一个满足某谓词，那么另一个也满足此谓词。

subst : ∀ {A : Set} {x y : A} (P : A → Set)
  → x ≡ y
    ---------
  → P x → P y
subst P refl px = px

谓词是对于某类型为 A 的值之上的命题；因为我们将命题视作类型， 谓词则是对于 A 参数化的一个类型。 例如，参考我们之前在 Relations 章节中的例子， even 和 odd 是自然数 ℕ 之上的谓词。 （我们将在 Decidable 章节中比较谓词的两种表示方式：以归纳数据类型 A → Set 或者以布尔值函数 A → Bool。）

等式链

我们在此演示如何使用等式链来论证，正如本书中使用证明形式。我们将声明放在一个叫做 ≡-Reasoning 的模块里，与 Agda 标准库中的格式相对应。

module ≡-Reasoning {A : Set} where

  infix   begin_
  infixr  _≡⟨⟩_ step-≡
  infix   _∎

  begin_ : ∀ {x y : A}
    → x ≡ y
      -----
    → x ≡ y
  begin x≡y  =  x≡y

  _≡⟨⟩_ : ∀ (x : A) {y : A}
    → x ≡ y
      -----
    → x ≡ y
  x ≡⟨⟩ x≡y  =  x≡y

  step-≡ : ∀ (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
  step-≡ x y≡z x≡y  =  trans x≡y y≡z

  syntax step-≡ x y≡z x≡y  =  x ≡⟨  x≡y ⟩ y≡z

  _∎ : ∀ (x : A)
      -----
    → x ≡ x
  x ∎  =  refl

open ≡-Reasoning

这是我们第一次使用嵌套的模块。它包括了关键字 module 和后续的模块名、隐式或显式参数， 关键字 where，和模块中的内容（在缩进内）。模块里可以包括任何形式的声明，也可以包括其他模块。 嵌套的模块和本书每章节所定义的顶层模块相似，只是顶层模块不需要缩进。 打开（open）一个模块会把模块内的所有定义导入进当前的环境中。

这也是我们第一次使用语法声明，它指明了左侧的项可以写成右边的语法形式。 语法 x ≡⟨ x≡y ⟩ y≡z 继承了声明 step-≡ 时使用的中缀式声明 infixr 2， 这种特殊的语法只要导入了 step-≡ 标识符就能使用。

除了引入带特殊语法的 step-≡ 外，我们也可以直接声明 _≡⟨_⟩′_：

_≡⟨_⟩′_ : ∀ {A : Set} (x : A) {y z : A}
  → x ≡ y
  → y ≡ z
    -----
  → x ≡ z
x ≡⟨ x≡y ⟩′ y≡z  =  trans x≡y y≡z

间接使用它的原因是 step-≡ 反转了实参的顺序，这样能让 Agda 更高效地执行类型推导。 在 Lambda 一章中我们会遇到一些长等式链，因此效率是很重要的。

我们来看看如何用等式链证明传递性：

trans′ : ∀ {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
    -----
  → x ≡ z
trans′ {A} {x} {y} {z} x≡y y≡z =
  begin
    x
  ≡⟨ x≡y ⟩
    y
  ≡⟨ y≡z ⟩
    z
  ∎

根据其定义，等式右边会被解析成如下：

begin (x ≡⟨ x≡y ⟩ (y ≡⟨ y≡z ⟩ (z ∎)))

这里 begin 的使用纯粹是装饰性的，因为它直接返回了其参数。其参数包括了 _≡⟨_⟩_ 作用于 x、x≡y 和 y ≡⟨ y≡z ⟩ (z ∎)。第一个参数是一个项 x， 而第二、第三个参数分别是等式 x ≡ y、y ≡ z 的证明，它们在 _≡⟨_⟩_ 的定义中用 trans 连接起来，形成 x ≡ z 的证明。y ≡ z 的证明包括了 _≡⟨_⟩_ 作用于 y、 y≡z 和 z ∎。第一个参数是一个项 y，而第二、第三个参数分别是等式 y ≡ z、z ≡ z 的证明， 它们在 _≡⟨_⟩_ 的定义中用 trans 连接起来，形成 y ≡ z 的证明。最后，z ≡ z 的证明包括了 _∎ 作用于 z 之上，使用了 refl。经过化简，上述定义等同于：

trans x≡y (trans y≡z refl)

我们可以把任意等式链转化成一系列的 trans 的使用。这样的证明更加精简，但是更难以阅读。 ∎ 的小窍门意味着等式链化简成为的一系列 trans 会以 trans e refl 结尾，尽管只需要 e 就足够了，这里的 e 是等式的证明。

Exercise trans and ≡-Reasoning (practice)

Sadly, we cannot use the definition of trans’ using ≡-Reasoning as the definition for trans. Can you see why? (Hint: look at the definition of _≡⟨_⟩_)

-- Your code goes here

等式链的另外一个例子

我们重新证明加法的交换律来作为等式链的第二个例子。我们首先重复自然数和加法的定义。 我们不能导入它们（正如本章节开头中所解释的那样），因为那样会产生一个冲突：

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero    + n  =  n
(suc m) + n  =  suc (m + n)

为了节约空间，我们假设两条引理（而不是证明它们）：

postulate
  +-identity : ∀ (m : ℕ) → m + zero ≡ m
  +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

这是我们第一次使用假设（Postulate）。假设为一个标识符指定一个签名，但是不提供定义。 我们在这里假设之前证明过的东西，来节约空间。假设在使用时必须加以注意。如果假设的内容为假， 那么我们可以证明出任何东西。

我们接下来重复交换律的证明：

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identity m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

论证的过程和之前的相似。我们在不需要解释的地方使用 _≡⟨⟩_，我们可以认为 _≡⟨⟩_ 和 _≡⟨ refl ⟩_ 是等价的。

Agda 总是认为一个项与其化简的项是等价的。我们之所以可以写出

  suc (n + m)
≡⟨⟩
  suc n + m

是因为 Agda 认为它们是一样的。这也意味着我们可以交换两行的顺序，写出

  suc n + m
≡⟨⟩
  suc (n + m)

而 Agda 并不会反对。Agda 只会检查由 ≡⟨⟩ 隔开的项是否化简后相同。 而书写的顺序合不合理则是由我们自行决定。

练习 ≤-Reasoning (延伸)

章节 Relations 中的单调性证明亦可以用相似于 ≡-Reasoning 的，更易于理解的形式给出。 相似地来定义 ≤-Reasoning，并用其重新给出加法对于不等式是单调的证明。重写 +-monoˡ-≤、+-monoʳ-≤ 和 +-mono-≤ 的定义。

-- 请将代码写在此处。

重写

考虑一个自然数的性质，比如说一个数是偶数。我们重复之前给出的定义：

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  even-zero : even zero

  even-suc : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where
  odd-suc : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

在前面的部分中，我们证明了加法满足交换律。给定 even (m + n) 成立的证据，我们应当可以用它来做 even (n + m) 成立的证据。

Agda 对这种论证有特殊记法的支持——我们之前提到过的 rewrite 记法。来启用这种记法， 我们只用编译程序指令来告诉 Agda 什么类型对应相等性：

{-# BUILTIN EQUALITY _≡_ #-}

我们然后就可以如下证明求证的性质：

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev  rewrite +-comm n m  =  ev

在这里，ev 包括了所有 even (m + n) 成立的证据，我们证明它亦可作为 even (n + m) 成立的证据。一般来说，关键字 rewrite 之后跟着一个等式的证明，这个等式被用于重写目标和任意作用域内变量的类型。

交互性地证明 even-comm 是很有帮助的。一开始，我们先给左边的参数赋予变量，给右手边放上一个洞：

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev = {! !}

如果我们进入洞里，输入 C-c C-,，Agda 会报告：

Goal: even (n + m)
————————————————————————————————————————————————————————————
ev : even (m + n)
n  : ℕ
m  : ℕ

现在我们加入重写：

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev rewrite +-comm n m = {! !}

如果我们再次进入洞里，并输入 C-c C-,，Agda 现在会报告：

Goal: even (m + n)
————————————————————————————————————————————————————————————
ev : even (m + n)
n  : ℕ
m  : ℕ

目标里的参数被交换了。现在 ev 显然满足目标条件，输入 C-c C-a 会用 ev 来填充这个洞。 命令 C-c C-a 可以进行自动搜索，检查作用域内的变量是否和目标有相同的类型。

多重重写

我们可以多次使用重写，以竖线隔开。举个例子，这里是加法交换律的第二个证明，使用重写而不是等式链：

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ zero    n  rewrite +-identity n             =  refl
+-comm′ (suc m) n  rewrite +-suc n m | +-comm′ m n  =  refl

这个证明更加的简短。之前的证明用 cong suc (+-comm m n) 作为使用归纳假设的说明， 而这里我们使用 +-comm m n 来重写就足够了，因为重写可以将合同性考虑在其中。尽管使用重写的证明更加的简短， 使用等式链的证明能容易理解，我们将尽可能的使用后者。

深入重写

rewrite 记法实际上是 with 抽象的一种应用：

even-comm′ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm′ m n ev with   m + n  | +-comm m n
...                  | .(n + m) | refl       = ev

总的来着，我们可以在 with 后面跟上任何数量的表达式，用竖线分隔开，并且在每个等式中使用相同个数的模式。 我们经常将表达式和模式如上对齐。这个第一列表明了 m + n 和 n + m 是相同的，第二列使用相应等式来证明的前述的断言。 注意在这里使用的点模式（Dot Pattern），.(n + m)。点模式由一个点和一个表达式组成， 在其他信息迫使这个值和点模式中的值相等时使用。在这里，m + n 和 n + m 由后续的 +-comm m n 与 refl 的匹配来识别。我们可能会认为第一种情况是多余的，因为第二种情况中才蕴涵了需要的信息。 但实际上 Agda 在这件事上很挑剔——省略第一条或者更换顺序会让 Agda 报告一个错误。（试一试你就知道！）

在这种情况中，我们也可以使用之前定义的替换函数来避免使用重写：

even-comm″ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm″ m n  =  subst even (+-comm m n)

尽管如此，重写是 Agda 工具箱中很重要的一部分。我们会偶尔使用它，但是它有的时候是必要的。

莱布尼兹（Leibniz）相等性

我们使用的相等性断言的形式源于 Martin-Löf，于 1975 年发表。一个更早的形式源于莱布尼兹， 于 1686 年发表。莱布尼兹断言的相等性表示不可分辨的实体（Identity of Indiscernibles）： 两个对象相等当且仅当它们满足完全相同的性质。这条原理有时被称作莱布尼兹定律（Leibniz’ Law）， 与史波克定律紧密相关：「一个不造成区别的区别不是区别」。我们在这里定义莱布尼兹相等性， 并证明两个项满足莱布尼兹相等性当且仅当其满足 Martin-Löf 相等性。

莱布尼兹相等性一般如下来定义：x ≐ y 当每个对于 x 成立的性质 P 对于 y 也成立时成立。 可能这有些出乎意料，但是这个定义亦足够保证其相反的命题：每个对于 y 成立的性质 P 对于 x 也成立。

令 x 和 y 为类型 A 的对象。我们定义 x ≐ y 成立，当每个对于类型 A 成立的谓词 P， 我们有 P x 蕴涵了 P y：

_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y

我们不能在左手边使用 x ≐ y，取而代之我们使用 _≐_ {A} x y 来提供隐式参数 A，这样 A 可以出现在右手边。

这是我们第一次使用等级（Levels）。我们不能将 Set 赋予类型 Set，因为这会导致自相矛盾， 比如罗素悖论（Russell’s Paradox）或者 Girard 悖论。不同的是，我们有一个阶级的类型：其中 Set : Set₁，Set₁ : Set₂，以此类推。实际上，Set 本身就是 Set₀ 的缩写。定义 _≐_ 的等式在右手边提到了 Set，因此签名中必须使用 Set₁。我们稍后将进一步介绍等级。

莱布尼兹相等性是自反和传递的。自反性由恒等函数的变种得来，传递性由函数组合的变种得来：

refl-≐ : ∀ {A : Set} {x : A}
  → x ≐ x
refl-≐ P Px  =  Px

trans-≐ : ∀ {A : Set} {x y z : A}
  → x ≐ y
  → y ≐ z
    -----
  → x ≐ z
trans-≐ x≐y y≐z P Px  =  y≐z P (x≐y P Px)

对称性就没有那么显然了。我们需要证明如果对于所有谓词 P，P x 蕴涵 P y， 那么反方向的蕴涵也成立。

sym-≐ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -----
  → y ≐ x
sym-≐ {A} {x} {y} x≐y P  =  Qy
  where
    Q : A → Set
    Q z = P z → P x
    Qx : Q x
    Qx = refl-≐ P
    Qy : Q y
    Qy = x≐y Q Qx

给定 x ≐ y 和一个特定的 P，我们需要构造一个 P y 蕴涵 P x 的证明。 我们首先用一个谓词 Q 将相等性实例化，使得 Q z 在 P z 蕴涵 P x 时成立。 Q x 这个性质是显然的，由自反性可以得出，由此通过 x ≐ y 就能推出 Q y 成立。而 Q y 正是我们需要的证明，即 P y 蕴涵 P x。

我们现在来证明 Martin-Löf 相等性蕴涵了莱布尼兹相等性，以及其逆命题。在正方向上， 如果我们已知 x ≡ y，我们需要对于任意的 P，将 P x 的证明转换为 P y 的证明。 我们很容易就可以做到这一点，因为 x 与 y 相等意味着任何 P x 的证明即是 P y 的证明。

≡-implies-≐ : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → x ≐ y
≡-implies-≐ x≡y P  =  subst P x≡y

因为这个方向由替换性可以得来，如之前证明的那样。

在反方向上，我们已知对于任何 P，我们可以将 P x 的证明转换成 P y 的证明， 我们需要证明 x ≡ y：

≐-implies-≡ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -----
  → x ≡ y
≐-implies-≡ {A} {x} {y} x≐y  =  Qy
  where
    Q : A → Set
    Q z = x ≡ z
    Qx : Q x
    Qx = refl
    Qy : Q y
    Qy = x≐y Q Qx

此证明与莱布尼兹相等性的对称性证明相似。我们取谓词 Q，使得 Q z 在 x ≡ z 成立时成立。 那么 Q x 是显然的，由 Martin Löf 相等性的自反性得来。从而 Q y 由 x ≐ y 可得， 而 Q y 即是我们所需要的 x ≡ y 的证明。

（本部分的内容由此处改编得来： ≐≃≡: Leibniz Equality is Isomorphic to Martin-Löf Identity, Parametrically 作者：Andreas Abel、Jesper Cockx、Dominique Devries、Andreas Nuyts 与 Philip Wadler， 草稿，2017）

全体多态

正如我们之前看到的那样，不是每个类型都属于 Set，但是每个类型都属于类型阶级的某处， Set₀、Set₁、Set₂等等。其中 Set 是 Set₀ 的缩写，此外 Set₀ : Set₁，Set₁ : Set₂，以此类推。 当我们需要比较两个属于 Set 的类型的值时，我们之前给出的定义是足够的， 但如果我们需要比较对于任何等级 ℓ，两个属于 Set ℓ 的类型的值该怎么办呢？

答案是全体多态（Universe Polymorphism），一个定义可以根据任何等级 ℓ 来做出。 为了使用等级，我们首先导入下列内容：

open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)

我们将构造子 zero 和 suc 重命名至 lzero 和 lsuc，为了防止自然数和等级之间的混淆。

等级与自然数是同构的，有相似的构造子：

lzero : Level
lsuc  : Level → Level

Set₀、Set₁、Set₂ 等名称，是下列的简写：

Set lzero
Set (lsuc lzero)
Set (lsuc (lsuc lzero))

以此类推。我们还有一个运算符：

_⊔_ : Level → Level → Level

给定两个等级，返回两者中较大的那个。

下面是相等性的定义，推广到任意等级：

data _≡′_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl′ : x ≡′ x

相似的，下面是对称性的推广定义：

sym′ : ∀ {ℓ : Level} {A : Set ℓ} {x y : A}
  → x ≡′ y
    ------
  → y ≡′ x
sym′ refl′ = refl′

为了简洁，我们在本书中给出的定义将避免使用全体多态，但是大多数标准库中的定义， 包括相等性的定义，都推广到了任意等级，如上所示。

下面是莱布尼兹相等性的推广定义：

_≐′_ : ∀ {ℓ : Level} {A : Set ℓ} (x y : A) → Set (lsuc ℓ)
_≐′_ {ℓ} {A} x y = ∀ (P : A → Set ℓ) → P x → P y

之前，签名中使用了 Set₁ 来作为一个值包括了 Set 的类型；而此处，我们使用 Set (lsuc ℓ) 来作为一个值包括了 Set ℓ 的类型。

标准库中的大部分函数都泛化到了任意层级。例如，以下是复合的定义。

_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
  → (B → C) → (A → B) → A → C
(g ∘ f) x  =  g (f x)

更多关于层级的信息可以从Agda 文档中查询。

标准库

标准库中可以找到与本章节中相似的定义。Agda 标准库将 _≡⟨_⟩_ 定义为 step-≡， 它反转了参数的顺序。标准库还定义了一个语法宏，它可以在你导入 step-≡ 时被自动导入，它能够恢复原始的参数顺序：

-- import Relation.Binary.PropositionalEquality as Eq
-- open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
-- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

这里的导入以注释的形式给出，以防止冲突，如引言中解释的那样。

Unicode

本章节使用下列 Unicode：

≡  U+2261  等同于 (\==, \equiv)
⟨  U+27E8  数学左尖括号 (\<)
⟩  U+27E9  数学右尖括号 (\>)
∎  U+220E  证毕 (\qed)
≐  U+2250  趋近于极限 (\.=)
ℓ  U+2113  手写小写 L (\ell)
⊔  U+2294  正方形向上开口 (\lub)
₀  U+2080  下标 0 (\_0)
₁  U+2081  下标 1 (\_1)
₂  U+2082  下标 2 (\_2)

Isomorphism: 同构与嵌入

module plfa.part1.Isomorphism where

本部分介绍同构（Isomorphism）与嵌入（Embedding）。 同构可以断言两个类型是相等的，嵌入可以断言一个类型比另一个类型小。 我们会在下一章中使用同构来展示类型上的运算，例如积或者和，满足类似于交换律、结合律和分配律的性质。

导入

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong-app)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

Lambda 表达式

本章节开头将补充一些有用的基础知识：lambda 表达式，函数组合，以及外延性。

Lambda 表达式提供了一种简洁的定义函数的方法，且不需要提供函数名。一个如同这样的项：

λ{ P₁ → N₁; ⋯ ; Pₙ → Nₙ }

等同于定义一个函数 f，使用下列等式：

f P₁ = N₁
⋯
f Pₙ = Nₙ

其中 Pₙ 是模式（即等式的左手边），Nₙ 是表达式（即等式的右手边）。

如果只有一个等式，且模式是一个变量，我们亦可使用下面的语法：

λ x → N

或者

λ (x : A) → N

两个都与 λ{x → N} 等价。后者可以指定函数的作用域。

往往使用匿名的 lambda 表达式比使用带名字的函数要方便：它避免了冗长的类型声明； 其定义出现在其使用的地方，所以在书写时不需要记得提前声明，在阅读时不需要上下搜索函数定义。

函数组合 （Function Composition）

接下来，我们将使用函数组合：

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘ f) x  = g (f x)

g ∘ f 是一个函数，先使用函数 f，再使用函数 g。 一个等价的定义，使用 lambda 表达式，如下：

_∘′_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
g ∘′ f  =  λ x → g (f x)

外延性（Extensionality）

外延性断言了区分函数的唯一方法是应用它们。如果两个函数作用在相同的参数上永远返回相同的结果， 那么两个函数相同。这是 cong-app 的逆命题，在之前有所介绍。

Agda 并不预设外延性，但我们可以假设其成立：

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

假设外延性不会造成困顿，因为我们知道它与 Agda 使用的理论是连贯一致的。

举个例子，我们考虑两个库都定义了加法，一个按照我们在 Naturals 章节中那样定义，另一个如下，反过来定义：

_+′_ : ℕ → ℕ → ℕ
m +′ zero  = m
m +′ suc n = suc (m +′ n)

通过使用交换律，我们可以简单地证明两个运算符在给定相同参数的情况下， 会返回相同的值：

same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n
same-app m n rewrite +-comm m n = helper m n
  where
  helper : ∀ (m n : ℕ) → m +′ n ≡ n + m
  helper m zero    = refl
  helper m (suc n) = cong suc (helper m n)

然而，有时断言两个运算符是无法区分的会更加方便。我们可以使用两次外延性：

same : _+′_ ≡ _+_
same = extensionality (λ m → extensionality (λ n → same-app m n))

我们偶尔需要在之后的情况中假设外延性。

postulate
  ∀-extensionality : ∀ {A : Set} {B : A → Set} {f g : ∀(x : A) → B x}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

Here the type of f and g has changed from A → B to ∀ (x : A) → B x, generalising ordinary functions to dependent functions.

同构（Isomorphism）

如果两个集合有一一对应的关系，那么它们是同构的。 下面是同构的正式定义：

infix  _≃_
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

我们来一一展开这个定义。一个集合 A 和 B 之间的同构有四个要素： 1. 从 A 到 B 的函数 to 2. 从 B 回到 A 的函数 from 3. from 是 to 的左逆（left-inverse）的证明 from∘to 4. from 是 to 的右逆（right-inverse）的证明 to∘from

具体来说，第三条断言了 from ∘ to 是恒等函数，第四条断言了 to ∘ from 是恒等函数， 它们的名称由此得来。声明 open _≃_ 使得 to、from、from∘to 和 to∘from 在当前作用域内可用，否则我们需要使用类似 _≃_.to 的写法。

这是我们第一次使用记录（Record）。记录声明的行为类似于一个单构造子的数据声明 （二者稍微有些不同，我们会在 Connectives 一章中讨论）：

data _≃′_ (A B : Set): Set where
  mk-≃′ : ∀ (to : A → B) →
          ∀ (from : B → A) →
          ∀ (from∘to : (∀ (x : A) → from (to x) ≡ x)) →
          ∀ (to∘from : (∀ (y : B) → to (from y) ≡ y)) →
          A ≃′ B

to′ : ∀ {A B : Set} → (A ≃′ B) → (A → B)
to′ (mk-≃′ f g g∘f f∘g) = f

from′ : ∀ {A B : Set} → (A ≃′ B) → (B → A)
from′ (mk-≃′ f g g∘f f∘g) = g

from∘to′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (x : A) → from′ A≃B (to′ A≃B x) ≡ x)
from∘to′ (mk-≃′ f g g∘f f∘g) = g∘f

to∘from′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (y : B) → to′ A≃B (from′ A≃B y) ≡ y)
to∘from′ (mk-≃′ f g g∘f f∘g) = f∘g

我们用下面的语法来构造一个记录类型的值：

record
  { to    = f
  ; from  = g
  ; from∘to = g∘f
  ; to∘from = f∘g
  }

这与使用相应的归纳类型的构造子对应：

mk-≃′ f g g∘f f∘g

其中 f、g、g∘f 和 f∘g 是相应类型的值。

同构是一个等价关系

同构是一个等价关系。这意味着它自反、对称、传递。要证明同构是自反的，我们用恒等函数 作为 to 和 from：

≃-refl : ∀ {A : Set}
    -----
  → A ≃ A
≃-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    ; to∘from = λ{y → refl}
    }

如上，to 和 from 都是恒等函数，from∘to 和 to∘from 都是丢弃参数、返回 refl 的函数。在这样的情况下，refl 足够可以证明左逆，因为 from (to x) 化简为 x。右逆的证明同理。

要证明同构是对称的，我们把 to 和 from、from∘to 和 to∘from 互换：

≃-sym : ∀ {A B : Set}
  → A ≃ B
    -----
  → B ≃ A
≃-sym A≃B =
  record
    { to      = from A≃B
    ; from    = to   A≃B
    ; from∘to = to∘from A≃B
    ; to∘from = from∘to A≃B
    }

要证明同构是传递的，我们将 to 和 from 函数进行组合，并使用相等性论证来结合左逆和右逆：

≃-trans : ∀ {A B C : Set}
  → A ≃ B
  → B ≃ C
    -----
  → A ≃ C
≃-trans A≃B B≃C =
  record
    { to       = to   B≃C ∘ to   A≃B
    ; from     = from A≃B ∘ from B≃C
    ; from∘to  = λ{x →
        begin
          (from A≃B ∘ from B≃C) ((to B≃C ∘ to A≃B) x)
        ≡⟨⟩
          from A≃B (from B≃C (to B≃C (to A≃B x)))
        ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩
          from A≃B (to A≃B x)
        ≡⟨ from∘to A≃B x ⟩
          x
        ∎}
    ; to∘from = λ{y →
        begin
          (to B≃C ∘ to A≃B) ((from A≃B ∘ from B≃C) y)
        ≡⟨⟩
          to B≃C (to A≃B (from A≃B (from B≃C y)))
        ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C y)) ⟩
          to B≃C (from B≃C y)
        ≡⟨ to∘from B≃C y ⟩
          y
        ∎}
     }

同构的相等性论证

我们可以直接的构造一种同构的相等性论证方法。我们对之前的相等性论证定义进行修改。 我们省略 _≡⟨⟩_ 的定义，因为简单的同构比简单的相等性出现的少很多：

module ≃-Reasoning where

  infix   ≃-begin_
  infixr  _≃⟨_⟩_
  infix   _≃-∎

  ≃-begin_ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≃ B
  ≃-begin A≃B = A≃B

  _≃⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≃ B
    → B ≃ C
      -----
    → A ≃ C
  A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

  _≃-∎ : ∀ (A : Set)
      -----
    → A ≃ A
  A ≃-∎ = ≃-refl

open ≃-Reasoning

嵌入（Embedding）

我们同时也需要嵌入的概念，它是同构的弱化概念。同构要求证明两个类型之间的一一对应， 而嵌入只需要第一种类型涵盖在第二种类型内，所以两个类型之间有一对多的对应关系。

嵌入的正式定义如下：

infix  _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

除了它缺少了 to∘from 字段以外，嵌入的定义和同构是一样的。因此，我们可以得知 from 是 to 的左逆，但是 from 不是 to 的右逆。

嵌入是自反和传递的，但不是对称的。证明与同构类似，不过去除了不需要的部分：

≲-refl : ∀ {A : Set} → A ≲ A
≲-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    }

≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
≲-trans A≲B B≲C =
  record
    { to      = λ{x → to   B≲C (to   A≲B x)}
    ; from    = λ{y → from A≲B (from B≲C y)}
    ; from∘to = λ{x →
        begin
          from A≲B (from B≲C (to B≲C (to A≲B x)))
        ≡⟨ cong (from A≲B) (from∘to B≲C (to A≲B x)) ⟩
          from A≲B (to A≲B x)
        ≡⟨ from∘to A≲B x ⟩
          x
        ∎}
     }

显而易见的是，如果两个类型相互嵌入，且其嵌入函数相互对应，那么它们是同构的。 这个一种反对称性的弱化形式：

≲-antisym : ∀ {A B : Set}
  → (A≲B : A ≲ B)
  → (B≲A : B ≲ A)
  → (to A≲B ≡ from B≲A)
  → (from A≲B ≡ to B≲A)
    -------------------
  → A ≃ B
≲-antisym A≲B B≲A to≡from from≡to =
  record
    { to      = to A≲B
    ; from    = from A≲B
    ; from∘to = from∘to A≲B
    ; to∘from = λ{y →
        begin
          to A≲B (from A≲B y)
        ≡⟨ cong (to A≲B) (cong-app from≡to y) ⟩
          to A≲B (to B≲A y)
        ≡⟨ cong-app to≡from (to B≲A y) ⟩
          from B≲A (to B≲A y)
        ≡⟨ from∘to B≲A y ⟩
          y
        ∎}
    }

前三部分可以直接从嵌入中得来，最后一部分我们可以把 B ≲ A 中的左逆和 两个嵌入中的 to 与 from 部分的相等性来获得同构中的右逆。

嵌入的相等性论证

和同构类似，我们亦支持嵌入的相等性论证：

module ≲-Reasoning where

  infix   ≲-begin_
  infixr  _≲⟨_⟩_
  infix   _≲-∎

  ≲-begin_ : ∀ {A B : Set}
    → A ≲ B
      -----
    → A ≲ B
  ≲-begin A≲B = A≲B

  _≲⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≲ B
    → B ≲ C
      -----
    → A ≲ C
  A ≲⟨ A≲B ⟩ B≲C = ≲-trans A≲B B≲C

  _≲-∎ : ∀ (A : Set)
      -----
    → A ≲ A
  A ≲-∎ = ≲-refl

open ≲-Reasoning

练习 ≃-implies-≲（实践）

证明每个同构蕴涵了一个嵌入。

postulate
  ≃-implies-≲ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≲ B

-- 请将代码写在此处。

练习 _⇔_（实践）

按下列形式定义命题的等价性（又名「当且仅当」）：

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A

证明等价性是自反、对称和传递的。

-- 请将代码写在此处。

练习 Bin-embedding （延伸）

回忆练习 Bin 和 Bin-laws， 我们定义了比特串数据类型 Bin 来表示自然数，并要求你来定义下列函数：

to : ℕ → Bin
from : Bin → ℕ

它们满足如下性质：

from (to n) ≡ n

使用上述条件，证明存在一个从 ℕ 到 Bin 的嵌入。

-- 请将代码写在此处。

为什么 to 和 from 不能构造一个同构？

标准库

标准库中可以找到与本章节中相似的定义：

import Function using (_∘_)
import Function.Inverse using (_↔_)
import Function.LeftInverse using (_↞_)